Theorem 3adant3r3 1184

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 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1171	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  infsupprpr  9498  ressress  17192  plttr  18294  plelttr  18296  latledi  18429  latmlej11  18430  latmlej21  18432  latmlej22  18433  latjass  18435  latj12  18436  latj31  18439  latdisdlem  18448  ipopos  18488  imasmnd2  18661  imasmnd  18662  grpaddsubass  18912  grpsubsub4  18915  grpnpncan  18917  imasgrp2  18937  imasgrp  18938  frgp0  19627  cmn12  19669  abladdsub  19679  imasring  20142  dvrass  20221  lss1  20548  islmhm2  20648  isdomn4  20917  zntoslem  21111  ipdir  21191  psrgrpOLD  21517  psrlmod  21520  t1sep  22873  mettri2  23846  xmetrtri  23860  xmetrtri2  23861  pi1grplem  24564  dchrabl  26754  motgrp  27791  xmstrkgc  28140  ax5seglem4  28187  grpomuldivass  29789  ablomuldiv  29800  ablodivdiv4  29802  nvmdi  29896  dipdi  30091  dipsubdir  30096  dipsubdi  30097  cgr3tr4  35019  cgr3rflx  35021  seglemin  35080  linerflx1  35116  elicc3  35197  rngosubdi  36808  rngosubdir  36809  igenval2  36929  dmncan1  36939  latmassOLD  38094  omlfh1N  38123  omlfh3N  38124  cvrnbtwn  38136  cvrnbtwn2  38140  cvrnbtwn4  38144  hlatj12  38236  cvrntr  38291  islpln2a  38414  3atnelvolN  38452  elpadd2at2  38673  paddasslem17  38702  paddass  38704  paddssw2  38710  pmapjlln1  38721  ltrn2ateq  39046  cdlemc3  39059  cdleme1b  39092  cdleme3b  39095  cdleme3c  39096  cdleme9b  39118  erngdvlem3  39856  erngdvlem3-rN  39864  dvalveclem  39891  mendlmod  41925  imasrng  46668  lincsumscmcl  47104