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  9502  ressress  17431  plttr  18520  plelttr  18522  latledi  18657  latmlej11  18658  latmlej21  18660  latmlej22  18661  latjass  18663  latj12  18664  latj31  18667  latdisdlem  18676  ipopos  18716  imasmnd2  18974  imasmnd  18975  grpaddsubass  19246  grpsubsub4  19249  grpnpncan  19251  imasgrp2  19271  imasgrp  19272  frgp0  19980  cmn12  20022  abladdsub  20032  imasrng  20405  imasring  20566  dvrass  20644  isdomn4  20973  lss1  21219  islmhm2  21319  unichnlidl  21522  rspprop  21530  zntoslem  21868  ipdir  21951  psrlmod  22273  t1sep  23694  mettri2  24666  xmetrtri  24680  xmetrtri2  24681  pi1grplem  25376  dchrabl  27587  motgrp  29012  xmstrkgc  29469  ax5seglem4  29516  grpomuldivass  31149  ablomuldiv  31160  ablodivdiv4  31162  nvmdi  31256  dipdi  31451  dipsubdir  31456  dipsubdi  31457  cgr3tr4  36910  cgr3rflx  36912  seglemin  36971  linerflx1  37007  elicc3  37198  rngosubdi  38973  rngosubdir  38974  igenval2  39094  dmncan1  39104  latmassOLD  40380  omlfh1N  40409  omlfh3N  40410  cvrnbtwn  40422  cvrnbtwn2  40426  cvrnbtwn4  40430  hlatj12  40522  cvrntr  40576  islpln2a  40699  3atnelvolN  40737  elpadd2at2  40958  paddasslem17  40987  paddass  40989  paddssw2  40995  pmapjlln1  41006  ltrn2ateq  41331  cdlemc3  41344  cdleme1b  41377  cdleme3b  41380  cdleme3c  41381  cdleme9b  41403  erngdvlem3  42141  erngdvlem3-rN  42149  dvalveclem  42176  mendlmod  44285  lincsumscmcl  49639