Theorem 3adant3r2 1197

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 1133	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr2 1184	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  plttr  18372  latjlej2  18486  latmlem1  18501  latmlem2  18502  latledi  18509  latmlej11  18510  latmlej12  18511  ipopos  18568  grppnpcan2  19076  mulgsubdir  19156  imasrng  20223  imasring  20375  isdomn4  20762  zntoslem  21605  mettri2  24398  mettri  24409  xmetrtri  24412  xmetrtri2  24413  metrtri  24414  ablomuldiv  30752  ablonnncan1  30757  nvmdi  30848  dipdi  31043  dipassr  31046  dipsubdir  31048  dipsubdi  31049  btwncomim  36360  cgr3tr4  36399  cgr3rflx  36401  colinbtwnle  36465  rngosubdi  38441  rngosubdir  38442  dmncan1  38572  dmncan2  38573  omlfh1N  39879  omlfh3N  39880  cvrnbtwn3  39897  cvrnbtwn4  39900  cvrcmp2  39905  hlatjrot  39994  cvrat3  40063  lplnribN  40172  ltrn2ateq  40801  dvalveclem  41646  mendlmod  43763