Theorem 3adant3r3 1182

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 1118	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1169	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  infsupprpr  9501  ressress  17197  plttr  18299  plelttr  18301  latledi  18434  latmlej11  18435  latmlej21  18437  latmlej22  18438  latjass  18440  latj12  18441  latj31  18444  latdisdlem  18453  ipopos  18493  imasmnd2  18696  imasmnd  18697  grpaddsubass  18949  grpsubsub4  18952  grpnpncan  18954  imasgrp2  18974  imasgrp  18975  frgp0  19669  cmn12  19711  abladdsub  19721  imasrng  20071  imasring  20218  dvrass  20299  lss1  20693  islmhm2  20793  isdomn4  21118  zntoslem  21331  ipdir  21411  psrgrpOLD  21737  psrlmod  21740  t1sep  23094  mettri2  24067  xmetrtri  24081  xmetrtri2  24082  pi1grplem  24796  dchrabl  26993  motgrp  28061  xmstrkgc  28410  ax5seglem4  28457  grpomuldivass  30061  ablomuldiv  30072  ablodivdiv4  30074  nvmdi  30168  dipdi  30363  dipsubdir  30368  dipsubdi  30369  cgr3tr4  35328  cgr3rflx  35330  seglemin  35389  linerflx1  35425  elicc3  35505  rngosubdi  37116  rngosubdir  37117  igenval2  37237  dmncan1  37247  latmassOLD  38402  omlfh1N  38431  omlfh3N  38432  cvrnbtwn  38444  cvrnbtwn2  38448  cvrnbtwn4  38452  hlatj12  38544  cvrntr  38599  islpln2a  38722  3atnelvolN  38760  elpadd2at2  38981  paddasslem17  39010  paddass  39012  paddssw2  39018  pmapjlln1  39029  ltrn2ateq  39354  cdlemc3  39367  cdleme1b  39400  cdleme3b  39403  cdleme3c  39404  cdleme9b  39426  erngdvlem3  40164  erngdvlem3-rN  40172  dvalveclem  40199  mendlmod  42237  lincsumscmcl  47201