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

Theorem 3ad2antr1 1180
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antr1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)

Proof of Theorem 3ad2antr1
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantrr 713 . 2 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
323adantr3 1163 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simpr1  1186  simpr1l  1222  simpr1r  1223  simpr11  1249  simpr12  1250  simpr13  1251  ispod  5475  funcnvqp  6411  dfwe2  7485  poxp  7811  cfcoflem  9682  axdc3lem  9860  fzadd2  12930  fzosubel2  13085  hashdifpr  13764  pfxccat3a  14088  sqr0lem  14588  iscatd2  16940  funcestrcsetclem9  17386  funcsetcestrclem9  17401  curf2cl  17469  yonedalem4c  17515  grpsubadd  18125  mulgnnass  18200  mulgnn0ass  18201  dprdss  19080  dprd2da  19093  srgi  19190  lsssn0  19648  psrbaglesupp  20076  zntoslem  20631  blsscls  23044  iimulcl  23468  pi1grplem  23580  pi1xfrf  23584  dvconst  24441  logexprlim  25728  wwlksnextbi  27599  clwwlkccatlem  27694  clwwlkccat  27695  umgr3cyclex  27889  nvss  28297  disjdsct  30364  issgon  31281  measdivcst  31382  measdivcstALTV  31383  prv1n  32575  elmrsubrn  32664  poimirlem28  34801  ftc1anc  34856  fdc  34901  cvrnbtwn3  36292  paddasslem9  36844  paddasslem17  36852  pmapjlln1  36871  lautj  37109  lautm  37110  dfsalgen2  42501  smflimlem4  42927  lidldomnnring  44129  funcringcsetcALTV2lem9  44243  funcringcsetclem9ALTV  44266  lincresunit3lem2  44463
  Copyright terms: Public domain W3C validator