Theorem 3adant3r3 1183

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 1119	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 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:  infsupprpr  9542  ressress  17294  plttr  18400  plelttr  18402  latledi  18535  latmlej11  18536  latmlej21  18538  latmlej22  18539  latjass  18541  latj12  18542  latj31  18545  latdisdlem  18554  ipopos  18594  imasmnd2  18800  imasmnd  18801  grpaddsubass  19061  grpsubsub4  19064  grpnpncan  19066  imasgrp2  19086  imasgrp  19087  frgp0  19793  cmn12  19835  abladdsub  19845  imasrng  20195  imasring  20344  dvrass  20425  isdomn4  20733  lss1  20954  islmhm2  21055  zntoslem  21593  ipdir  21675  psrgrpOLD  21995  psrlmod  21998  t1sep  23394  mettri2  24367  xmetrtri  24381  xmetrtri2  24382  pi1grplem  25096  dchrabl  27313  motgrp  28566  xmstrkgc  28915  ax5seglem4  28962  grpomuldivass  30570  ablomuldiv  30581  ablodivdiv4  30583  nvmdi  30677  dipdi  30872  dipsubdir  30877  dipsubdi  30878  cgr3tr4  36034  cgr3rflx  36036  seglemin  36095  linerflx1  36131  elicc3  36300  rngosubdi  37932  rngosubdir  37933  igenval2  38053  dmncan1  38063  latmassOLD  39211  omlfh1N  39240  omlfh3N  39241  cvrnbtwn  39253  cvrnbtwn2  39257  cvrnbtwn4  39261  hlatj12  39353  cvrntr  39408  islpln2a  39531  3atnelvolN  39569  elpadd2at2  39790  paddasslem17  39819  paddass  39821  paddssw2  39827  pmapjlln1  39838  ltrn2ateq  40163  cdlemc3  40176  cdleme1b  40209  cdleme3b  40212  cdleme3c  40213  cdleme9b  40235  erngdvlem3  40973  erngdvlem3-rN  40981  dvalveclem  41008  mendlmod  43178  lincsumscmcl  48279