Theorem 3adant3r3 1185

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 1172	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  9415  ressress  17176  plttr  18264  plelttr  18266  latledi  18401  latmlej11  18402  latmlej21  18404  latmlej22  18405  latjass  18407  latj12  18408  latj31  18411  latdisdlem  18420  ipopos  18460  imasmnd2  18666  imasmnd  18667  grpaddsubass  18927  grpsubsub4  18930  grpnpncan  18932  imasgrp2  18952  imasgrp  18953  frgp0  19657  cmn12  19699  abladdsub  19709  imasrng  20080  imasring  20233  dvrass  20311  isdomn4  20619  lss1  20859  islmhm2  20960  zntoslem  21481  ipdir  21564  psrgrpOLD  21882  psrlmod  21885  t1sep  23273  mettri2  24245  xmetrtri  24259  xmetrtri2  24260  pi1grplem  24965  dchrabl  27181  motgrp  28506  xmstrkgc  28849  ax5seglem4  28895  grpomuldivass  30503  ablomuldiv  30514  ablodivdiv4  30516  nvmdi  30610  dipdi  30805  dipsubdir  30810  dipsubdi  30811  cgr3tr4  36028  cgr3rflx  36030  seglemin  36089  linerflx1  36125  elicc3  36293  rngosubdi  37927  rngosubdir  37928  igenval2  38048  dmncan1  38058  latmassOLD  39210  omlfh1N  39239  omlfh3N  39240  cvrnbtwn  39252  cvrnbtwn2  39256  cvrnbtwn4  39260  hlatj12  39352  cvrntr  39407  islpln2a  39530  3atnelvolN  39568  elpadd2at2  39789  paddasslem17  39818  paddass  39820  paddssw2  39826  pmapjlln1  39837  ltrn2ateq  40162  cdlemc3  40175  cdleme1b  40208  cdleme3b  40211  cdleme3c  40212  cdleme9b  40234  erngdvlem3  40972  erngdvlem3-rN  40980  dvalveclem  41007  mendlmod  43165  lincsumscmcl  48422