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  9535  ressress  17469  plttr  18564  plelttr  18566  latledi  18701  latmlej11  18702  latmlej21  18704  latmlej22  18705  latjass  18707  latj12  18708  latj31  18711  latdisdlem  18720  ipopos  18760  imasmnd2  19018  imasmnd  19019  grpaddsubass  19290  grpsubsub4  19293  grpnpncan  19295  imasgrp2  19315  imasgrp  19316  frgp0  20025  cmn12  20067  abladdsub  20077  imasrng  20450  imasring  20611  dvrass  20689  isdomn4  21018  lss1  21264  islmhm2  21364  unichnlidl  21567  rspprop  21575  zntoslem  21917  ipdir  22000  psrlmod  22322  t1sep  23743  mettri2  24715  xmetrtri  24729  xmetrtri2  24730  pi1grplem  25425  dchrabl  27638  motgrp  29063  xmstrkgc  29520  ax5seglem4  29567  grpomuldivass  31200  ablomuldiv  31211  ablodivdiv4  31213  nvmdi  31307  dipdi  31502  dipsubdir  31507  dipsubdi  31508  cgr3tr4  37032  cgr3rflx  37034  seglemin  37093  linerflx1  37129  elicc3  37320  rngosubdi  39145  rngosubdir  39146  igenval2  39266  dmncan1  39276  latmassOLD  40552  omlfh1N  40581  omlfh3N  40582  cvrnbtwn  40594  cvrnbtwn2  40598  cvrnbtwn4  40602  hlatj12  40694  cvrntr  40748  islpln2a  40871  3atnelvolN  40909  elpadd2at2  41130  paddasslem17  41159  paddass  41161  paddssw2  41167  pmapjlln1  41178  ltrn2ateq  41503  cdlemc3  41516  cdleme1b  41549  cdleme3b  41552  cdleme3c  41553  cdleme9b  41575  erngdvlem3  42313  erngdvlem3-rN  42321  dvalveclem  42348  mendlmod  44452  lincsumscmcl  49876