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  9084  ccatswrd  14590  plttr  18261  pltletr  18262  latjlej1  18374  latjlej2  18375  latnlej  18377  latnlej2  18380  latmlem2  18391  latledi  18398  latjass  18404  latj32  18406  latj13  18407  ipopos  18457  tsrlemax  18507  imasmnd2  18697  grpsubsub  18957  grpnnncan2  18965  imasgrp2  18983  mulgnn0ass  19038  mulgsubdir  19042  cmn32  19727  ablsubadd  19736  imasrng  20110  imasring  20264  isdomn4  20647  zntoslem  21509  xmettri3  24295  mettri3  24296  xmetrtri  24297  xmetrtri2  24298  metrtri  24299  cphdivcl  25136  cphassr  25166  relogbmulexp  26742  grpodivdiv  30564  grpomuldivass  30565  ablo32  30573  ablodivdiv4  30578  ablodiv32  30579  nvmdi  30672  dipdi  30867  dipassr  30870  dipsubdir  30872  dipsubdi  30873  dvrcan5  33267  cgr3tr4  36195  cgr3rflx  36197  endofsegid  36228  seglemin  36256  broutsideof2  36265  rngosubdi  38085  rngosubdir  38086  isdrngo2  38098  crngm23  38142  dmncan2  38217  latmassOLD  39428  latm32  39430  cvrnbtwn4  39478  cvrcmp2  39483  ltcvrntr  39623  atcvrj0  39627  3dim3  39668  paddasslem17  40035  paddass  40037  lautlt  40290  lautcvr  40291  lautj  40292  lautm  40293  erngdvlem3  41189  dvalveclem  41224  mendlmod  43373