Theorem 3adant3r3 1203

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  infsupprpr  9469  ressress  17324  plttr  18413  plelttr  18415  latledi  18550  latmlej11  18551  latmlej21  18553  latmlej22  18554  latjass  18556  latj12  18557  latj31  18560  latdisdlem  18569  ipopos  18609  imasmnd2  18855  imasmnd  18856  grpaddsubass  19119  grpsubsub4  19122  grpnpncan  19124  imasgrp2  19144  imasgrp  19145  frgp0  19853  cmn12  19895  abladdsub  19905  imasrng  20278  imasring  20437  dvrass  20515  isdomn4  20843  lss1  21088  islmhm2  21188  unichnlidl  21391  rspprop  21399  zntoslem  21735  ipdir  21818  psrlmod  22138  t1sep  23556  mettri2  24527  xmetrtri  24541  xmetrtri2  24542  pi1grplem  25237  dchrabl  27447  motgrp  28841  xmstrkgc  29264  ax5seglem4  29311  grpomuldivass  30922  ablomuldiv  30933  ablodivdiv4  30935  nvmdi  31029  dipdi  31224  dipsubdir  31229  dipsubdi  31230  cgr3tr4  36557  cgr3rflx  36559  seglemin  36618  linerflx1  36654  elicc3  36861  rngosubdi  38629  rngosubdir  38630  igenval2  38750  dmncan1  38760  latmassOLD  40036  omlfh1N  40065  omlfh3N  40066  cvrnbtwn  40078  cvrnbtwn2  40082  cvrnbtwn4  40086  hlatj12  40178  cvrntr  40232  islpln2a  40355  3atnelvolN  40393  elpadd2at2  40614  paddasslem17  40643  paddass  40645  paddssw2  40651  pmapjlln1  40662  ltrn2ateq  40987  cdlemc3  41000  cdleme1b  41033  cdleme3b  41036  cdleme3c  41037  cdleme9b  41059  erngdvlem3  41797  erngdvlem3-rN  41805  dvalveclem  41832  mendlmod  43949  lincsumscmcl  49246