Theorem 3adant3r2 1199

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adant3r2

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1114	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1176	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074

This theorem is referenced by:  plttr  17192  latjlej2  17288  latmlem1  17303  latmlem2  17304  latledi  17311  latmlej11  17312  latmlej12  17313  ipopos  17382  grppnpcan2  17731  mulgsubdir  17804  imasring  18840  zntoslem  20128  mettri2  22368  mettri  22379  xmetrtri  22382  xmetrtri2  22383  metrtri  22384  ablomuldiv  27737  ablonnncan1  27743  nvmdi  27834  dipdi  28029  dipassr  28032  dipsubdir  28034  dipsubdi  28035  btwncomim  32448  cgr3tr4  32487  cgr3rflx  32489  colinbtwnle  32553  rngosubdi  34076  rngosubdir  34077  dmncan1  34207  dmncan2  34208  omlfh1N  35067  omlfh3N  35068  cvrnbtwn3  35085  cvrnbtwn4  35088  cvrcmp2  35093  hlatjrot  35181  cvrat3  35250  lplnribN  35359  ltrn2ateq  35989  dvalveclem  36835  mendlmod  38284