Theorem 3adant3r2 1184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  plttr  18277  latjlej2  18389  latmlem1  18404  latmlem2  18405  latledi  18412  latmlej11  18413  latmlej12  18414  ipopos  18471  grppnpcan2  18942  mulgsubdir  19022  imasrng  20062  imasring  20215  isdomn4  20601  zntoslem  21442  mettri2  24205  mettri  24216  xmetrtri  24219  xmetrtri2  24220  metrtri  24221  ablomuldiv  30454  ablonnncan1  30459  nvmdi  30550  dipdi  30745  dipassr  30748  dipsubdir  30750  dipsubdi  30751  btwncomim  35974  cgr3tr4  36013  cgr3rflx  36015  colinbtwnle  36079  rngosubdi  37912  rngosubdir  37913  dmncan1  38043  dmncan2  38044  omlfh1N  39224  omlfh3N  39225  cvrnbtwn3  39242  cvrnbtwn4  39245  cvrcmp2  39250  hlatjrot  39339  cvrat3  39409  lplnribN  39518  ltrn2ateq  40147  dvalveclem  40992  mendlmod  43151