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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  infsupprpr  9467  ressress  17308  plttr  18397  plelttr  18399  latledi  18534  latmlej11  18535  latmlej21  18537  latmlej22  18538  latjass  18540  latj12  18541  latj31  18544  latdisdlem  18553  ipopos  18593  imasmnd2  18833  imasmnd  18834  grpaddsubass  19097  grpsubsub4  19100  grpnpncan  19102  imasgrp2  19122  imasgrp  19123  frgp0  19831  cmn12  19873  abladdsub  19883  imasrng  20256  imasring  20413  dvrass  20491  isdomn4  20801  lss1  21040  islmhm2  21140  unichnlidl  21343  rspprop  21351  zntoslem  21687  ipdir  21770  psrlmod  22090  t1sep  23508  mettri2  24479  xmetrtri  24493  xmetrtri2  24494  pi1grplem  25189  dchrabl  27399  motgrp  28793  xmstrkgc  29216  ax5seglem4  29263  grpomuldivass  30874  ablomuldiv  30885  ablodivdiv4  30887  nvmdi  30981  dipdi  31176  dipsubdir  31181  dipsubdi  31182  cgr3tr4  36525  cgr3rflx  36527  seglemin  36586  linerflx1  36622  elicc3  36809  rngosubdi  38577  rngosubdir  38578  igenval2  38698  dmncan1  38708  latmassOLD  39984  omlfh1N  40013  omlfh3N  40014  cvrnbtwn  40026  cvrnbtwn2  40030  cvrnbtwn4  40034  hlatj12  40126  cvrntr  40180  islpln2a  40303  3atnelvolN  40341  elpadd2at2  40562  paddasslem17  40591  paddass  40593  paddssw2  40599  pmapjlln1  40610  ltrn2ateq  40935  cdlemc3  40948  cdleme1b  40981  cdleme3b  40984  cdleme3c  40985  cdleme9b  41007  erngdvlem3  41745  erngdvlem3-rN  41753  dvalveclem  41780  mendlmod  43899  lincsumscmcl  49196