Theorem 3adant3r2 1296

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r2

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1285	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1241	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

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

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 1056

This theorem is referenced by:  plttr  17017  latjlej2  17113  latmlem1  17128  latmlem2  17129  latledi  17136  latmlej11  17137  latmlej12  17138  ipopos  17207  grppnpcan2  17556  mulgsubdir  17629  imasring  18665  zntoslem  19953  mettri2  22193  mettri  22204  xmetrtri  22207  xmetrtri2  22208  metrtri  22209  ablomuldiv  27534  ablonnncan1  27540  nvmdi  27631  dipdi  27826  dipassr  27829  dipsubdir  27831  dipsubdi  27832  btwncomim  32245  cgr3tr4  32284  cgr3rflx  32286  colinbtwnle  32350  rngosubdi  33874  rngosubdir  33875  dmncan1  34005  dmncan2  34006  omlfh1N  34863  omlfh3N  34864  cvrnbtwn3  34881  cvrnbtwn4  34884  cvrcmp2  34889  hlatjrot  34977  cvrat3  35046  lplnribN  35155  ltrn2ateq  35785  dvalveclem  36631  mendlmod  38080