Theorem 3adant3r1 1181

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1168	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  9198  ccatswrd  14702  plttr  18399  pltletr  18400  latjlej1  18510  latjlej2  18511  latnlej  18513  latnlej2  18516  latmlem2  18527  latledi  18534  latjass  18540  latj32  18542  latj13  18543  ipopos  18593  tsrlemax  18643  imasmnd2  18799  grpsubsub  19059  grpnnncan2  19067  imasgrp2  19085  mulgnn0ass  19140  mulgsubdir  19144  cmn32  19832  ablsubadd  19841  imasrng  20194  imasring  20343  isdomn4  20732  zntoslem  21592  xmettri3  24378  mettri3  24379  xmetrtri  24380  xmetrtri2  24381  metrtri  24382  cphdivcl  25229  cphassr  25259  relogbmulexp  26835  grpodivdiv  30568  grpomuldivass  30569  ablo32  30577  ablodivdiv4  30582  ablodiv32  30583  nvmdi  30676  dipdi  30871  dipassr  30874  dipsubdir  30876  dipsubdi  30877  dvrcan5  33225  cgr3tr4  36033  cgr3rflx  36035  endofsegid  36066  seglemin  36094  broutsideof2  36103  rngosubdi  37931  rngosubdir  37932  isdrngo2  37944  crngm23  37988  dmncan2  38063  latmassOLD  39210  latm32  39212  cvrnbtwn4  39260  cvrcmp2  39265  ltcvrntr  39406  atcvrj0  39410  3dim3  39451  paddasslem17  39818  paddass  39820  lautlt  40073  lautcvr  40074  lautj  40075  lautm  40076  erngdvlem3  40972  dvalveclem  41007  mendlmod  43177