Theorem 3adant3r1 1274

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1266	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1220	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  plttr  16970  pltletr  16971  latjlej1  17065  latjlej2  17066  latnlej  17068  latnlej2  17071  latmlem2  17082  latledi  17089  latjass  17095  latj32  17097  latj13  17098  ipopos  17160  tsrlemax  17220  imasmnd2  17327  grpsubsub  17504  grpnnncan2  17512  imasgrp2  17530  mulgnn0ass  17578  mulgsubdir  17582  cmn32  18211  ablsubadd  18217  imasring  18619  zntoslem  19905  xmettri3  22158  mettri3  22159  xmetrtri  22160  xmetrtri2  22161  metrtri  22162  cphdivcl  22982  cphassr  23012  relogbmulexp  24516  grpodivdiv  27394  grpomuldivass  27395  ablo32  27403  ablodivdiv4  27408  ablodiv32  27409  ablonnncan  27410  nvmdi  27503  dipdi  27698  dipassr  27701  dipsubdir  27703  dipsubdi  27704  dvrcan5  29793  cgr3tr4  32159  cgr3rflx  32161  endofsegid  32192  seglemin  32220  broutsideof2  32229  rngosubdi  33744  rngosubdir  33745  isdrngo2  33757  crngm23  33801  dmncan2  33876  latmassOLD  34516  latm32  34518  cvrnbtwn4  34566  cvrcmp2  34571  ltcvrntr  34710  atcvrj0  34714  3dim3  34755  paddasslem17  35122  paddass  35124  lautlt  35377  lautcvr  35378  lautj  35379  lautm  35380  erngdvlem3  36278  dvalveclem  36314  mendlmod  37763