Theorem 3adant3r3 1276

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1266	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1222	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:  ressress  15938  plttr  16970  plelttr  16972  latledi  17089  latmlej11  17090  latmlej21  17092  latmlej22  17093  latjass  17095  latj12  17096  latj31  17099  ipopos  17160  latdisdlem  17189  imasmnd2  17327  imasmnd  17328  grpaddsubass  17505  grpsubsub4  17508  grpnpncan  17510  imasgrp2  17530  imasgrp  17531  frgp0  18173  cmn12  18213  abladdsub  18220  imasring  18619  dvrass  18690  lss1  18939  islmhm2  19038  psrgrp  19398  psrlmod  19401  zntoslem  19905  ipdir  19984  t1sep  21174  mettri2  22146  xmetrtri  22160  xmetrtri2  22161  pi1grplem  22849  dchrabl  24979  motgrp  25438  xmstrkgc  25766  ax5seglem4  25812  grpomuldivass  27395  ablomuldiv  27406  ablodivdiv4  27408  nvmdi  27503  dipdi  27698  dipsubdir  27703  dipsubdi  27704  cgr3tr4  32159  cgr3rflx  32161  seglemin  32220  linerflx1  32256  elicc3  32311  rngosubdi  33744  rngosubdir  33745  igenval2  33865  dmncan1  33875  latmassOLD  34516  omlfh1N  34545  omlfh3N  34546  cvrnbtwn  34558  cvrnbtwn2  34562  cvrnbtwn4  34566  hlatj12  34657  cvrntr  34711  islpln2a  34834  3atnelvolN  34872  elpadd2at2  35093  paddasslem17  35122  paddass  35124  paddssw2  35130  pmapjlln1  35141  ltrn2ateq  35467  cdlemc3  35480  cdleme1b  35513  cdleme3b  35516  cdleme3c  35517  cdleme9b  35539  erngdvlem3  36278  erngdvlem3-rN  36286  dvalveclem  36314  mendlmod  37763  lincsumscmcl  42222