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

Theorem 3ad2antr1 1218
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 748 . 2 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
323adantr3 1214 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  ispod  4957  funcnvqp  5852  dfwe2  6850  poxp  7153  cfcoflem  8954  axdc3lem  9132  fzadd2  12202  fzosubel2  12350  hashdifpr  13016  sqr0lem  13775  iscatd2  16111  funcestrcsetclem9  16557  funcsetcestrclem9  16572  curf2cl  16640  yonedalem4c  16686  grpsubadd  17272  mulgnnass  17345  mulgnnassOLD  17346  mulgnn0ass  17347  dprdss  18197  dprd2da  18210  srgi  18280  lsssn0  18715  psrbaglesupp  19135  zntoslem  19669  blsscls  22063  iimulcl  22475  pi1grplem  22588  pi1xfrf  22592  dvconst  23403  logexprlim  24667  constr3trllem1  25944  wwlknextbi  26019  nvss  26616  disjdsct  28669  issgon  29319  measdivcstOLD  29420  measdivcst  29421  elmrsubrn  30477  poimirlem28  32410  ftc1anc  32466  fdc  32514  cvrnbtwn3  33384  paddasslem9  33935  paddasslem17  33943  pmapjlln1  33962  lautj  34200  lautm  34201  dfsalgen2  39039  smflimlem4  39464  pfxccat3a  40097  splvalpfx  40103  wwlksnextbi  41102  umgr3cyclex  41352  lidldomnnring  41722  funcringcsetcALTV2lem9  41838  funcringcsetclem9ALTV  41861  lincresunit3lem2  42065
  Copyright terms: Public domain W3C validator