MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant3r3 Structured version   Visualization version   GIF version

Theorem 3adant3r3 1228
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
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1142 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1205 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  ressress  16150  plttr  17175  plelttr  17177  latledi  17294  latmlej11  17295  latmlej21  17297  latmlej22  17298  latjass  17300  latj12  17301  latj31  17304  ipopos  17365  latdisdlem  17394  imasmnd2  17532  imasmnd  17533  grpaddsubass  17710  grpsubsub4  17713  grpnpncan  17715  imasgrp2  17735  imasgrp  17736  frgp0  18374  cmn12  18414  abladdsub  18421  imasring  18821  dvrass  18892  lss1  19143  islmhm2  19245  psrgrp  19607  psrlmod  19610  zntoslem  20112  ipdir  20194  t1sep  21388  mettri2  22359  xmetrtri  22373  xmetrtri2  22374  pi1grplem  23061  dchrabl  25193  motgrp  25652  xmstrkgc  25980  ax5seglem4  26026  grpomuldivass  27724  ablomuldiv  27735  ablodivdiv4  27737  nvmdi  27831  dipdi  28026  dipsubdir  28031  dipsubdi  28032  cgr3tr4  32480  cgr3rflx  32482  seglemin  32541  linerflx1  32577  elicc3  32632  rngosubdi  34055  rngosubdir  34056  igenval2  34176  dmncan1  34186  latmassOLD  35009  omlfh1N  35038  omlfh3N  35039  cvrnbtwn  35051  cvrnbtwn2  35055  cvrnbtwn4  35059  hlatj12  35151  cvrntr  35205  islpln2a  35328  3atnelvolN  35366  elpadd2at2  35587  paddasslem17  35616  paddass  35618  paddssw2  35624  pmapjlln1  35635  ltrn2ateq  35961  cdlemc3  35974  cdleme1b  36007  cdleme3b  36010  cdleme3c  36011  cdleme9b  36033  erngdvlem3  36771  erngdvlem3-rN  36779  dvalveclem  36806  mendlmod  38264  lincsumscmcl  42790
  Copyright terms: Public domain W3C validator