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

Theorem 3ad2antr1 1232
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 699 . 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:  simpr1  1241  simpr1l  1298  simpr1r  1300  simpr11  1340  simpr12  1342  simpr13  1344  ispod  5240  funcnvqp  6164  dfwe2  7211  poxp  7523  cfcoflem  9379  axdc3lem  9557  fzadd2  12599  fzosubel2  12752  hashdifpr  13420  sqr0lem  14204  iscatd2  16546  funcestrcsetclem9  16993  funcsetcestrclem9  17008  curf2cl  17076  yonedalem4c  17122  grpsubadd  17708  mulgnnass  17779  mulgnn0ass  17780  dprdss  18630  dprd2da  18643  srgi  18713  lsssn0  19152  psrbaglesupp  19577  zntoslem  20112  blsscls  22525  iimulcl  22949  pi1grplem  23061  pi1xfrf  23065  dvconst  23894  logexprlim  25164  wwlksnextbi  27031  umgr3cyclex  27356  nvss  27776  disjdsct  29807  issgon  30511  measdivcstOLD  30612  measdivcst  30613  elmrsubrn  31740  poimirlem28  33750  ftc1anc  33805  fdc  33852  cvrnbtwn3  35056  paddasslem9  35608  paddasslem17  35616  pmapjlln1  35635  lautj  35873  lautm  35874  dfsalgen2  41038  smflimlem4  41464  pfxccat3a  42004  splvalpfx  42010  lidldomnnring  42498  funcringcsetcALTV2lem9  42612  funcringcsetclem9ALTV  42635  lincresunit3lem2  42837
  Copyright terms: Public domain W3C validator