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

This theorem is referenced by:  infsupprpr  9307  ressress  17003  plttr  18105  plelttr  18107  latledi  18240  latmlej11  18241  latmlej21  18243  latmlej22  18244  latjass  18246  latj12  18247  latj31  18250  latdisdlem  18259  ipopos  18299  imasmnd2  18467  imasmnd  18468  grpaddsubass  18710  grpsubsub4  18713  grpnpncan  18715  imasgrp2  18735  imasgrp  18736  frgp0  19411  cmn12  19452  abladdsub  19461  imasring  19903  dvrass  19977  lss1  20245  islmhm2  20345  zntoslem  20809  ipdir  20889  psrgrp  21212  psrlmod  21215  t1sep  22566  mettri2  23539  xmetrtri  23553  xmetrtri2  23554  pi1grplem  24257  dchrabl  26447  motgrp  26949  xmstrkgc  27298  ax5seglem4  27345  grpomuldivass  28948  ablomuldiv  28959  ablodivdiv4  28961  nvmdi  29055  dipdi  29250  dipsubdir  29255  dipsubdi  29256  cgr3tr4  34399  cgr3rflx  34401  seglemin  34460  linerflx1  34496  elicc3  34551  rngosubdi  36147  rngosubdir  36148  igenval2  36268  dmncan1  36278  latmassOLD  37285  omlfh1N  37314  omlfh3N  37315  cvrnbtwn  37327  cvrnbtwn2  37331  cvrnbtwn4  37335  hlatj12  37427  cvrntr  37481  islpln2a  37604  3atnelvolN  37642  elpadd2at2  37863  paddasslem17  37892  paddass  37894  paddssw2  37900  pmapjlln1  37911  ltrn2ateq  38236  cdlemc3  38249  cdleme1b  38282  cdleme3b  38285  cdleme3c  38286  cdleme9b  38308  erngdvlem3  39046  erngdvlem3-rN  39054  dvalveclem  39081  isdomn4  40214  mendlmod  41056  lincsumscmcl  45832