Theorem 3adant3r3 1200

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1114	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1177	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  ressress  16140  plttr  17171  plelttr  17173  latledi  17290  latmlej11  17291  latmlej21  17293  latmlej22  17294  latjass  17296  latj12  17297  latj31  17300  ipopos  17361  latdisdlem  17390  imasmnd2  17528  imasmnd  17529  grpaddsubass  17706  grpsubsub4  17709  grpnpncan  17711  imasgrp2  17731  imasgrp  17732  frgp0  18373  cmn12  18413  abladdsub  18420  imasring  18819  dvrass  18890  lss1  19141  islmhm2  19240  psrgrp  19600  psrlmod  19603  zntoslem  20107  ipdir  20186  t1sep  21376  mettri2  22347  xmetrtri  22361  xmetrtri2  22362  pi1grplem  23049  dchrabl  25178  motgrp  25637  xmstrkgc  25965  ax5seglem4  26011  grpomuldivass  27704  ablomuldiv  27715  ablodivdiv4  27717  nvmdi  27812  dipdi  28007  dipsubdir  28012  dipsubdi  28013  cgr3tr4  32465  cgr3rflx  32467  seglemin  32526  linerflx1  32562  elicc3  32617  rngosubdi  34057  rngosubdir  34058  igenval2  34178  dmncan1  34188  latmassOLD  35019  omlfh1N  35048  omlfh3N  35049  cvrnbtwn  35061  cvrnbtwn2  35065  cvrnbtwn4  35069  hlatj12  35160  cvrntr  35214  islpln2a  35337  3atnelvolN  35375  elpadd2at2  35596  paddasslem17  35625  paddass  35627  paddssw2  35633  pmapjlln1  35644  ltrn2ateq  35970  cdlemc3  35983  cdleme1b  36016  cdleme3b  36019  cdleme3c  36020  cdleme9b  36042  erngdvlem3  36780  erngdvlem3-rN  36788  dvalveclem  36816  mendlmod  38265  lincsumscmcl  42732