Theorem 3adant3r1 1183

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1170	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:  dif1en  9101  ccatswrd  14609  plttr  18277  pltletr  18278  latjlej1  18388  latjlej2  18389  latnlej  18391  latnlej2  18394  latmlem2  18405  latledi  18412  latjass  18418  latj32  18420  latj13  18421  ipopos  18471  tsrlemax  18521  imasmnd2  18677  grpsubsub  18937  grpnnncan2  18945  imasgrp2  18963  mulgnn0ass  19018  mulgsubdir  19022  cmn32  19706  ablsubadd  19715  imasrng  20062  imasring  20215  isdomn4  20601  zntoslem  21442  xmettri3  24217  mettri3  24218  xmetrtri  24219  xmetrtri2  24220  metrtri  24221  cphdivcl  25058  cphassr  25088  relogbmulexp  26664  grpodivdiv  30442  grpomuldivass  30443  ablo32  30451  ablodivdiv4  30456  ablodiv32  30457  nvmdi  30550  dipdi  30745  dipassr  30748  dipsubdir  30750  dipsubdi  30751  dvrcan5  33160  cgr3tr4  36013  cgr3rflx  36015  endofsegid  36046  seglemin  36074  broutsideof2  36083  rngosubdi  37912  rngosubdir  37913  isdrngo2  37925  crngm23  37969  dmncan2  38044  latmassOLD  39195  latm32  39197  cvrnbtwn4  39245  cvrcmp2  39250  ltcvrntr  39391  atcvrj0  39395  3dim3  39436  paddasslem17  39803  paddass  39805  lautlt  40058  lautcvr  40059  lautj  40060  lautm  40061  erngdvlem3  40957  dvalveclem  40992  mendlmod  43151