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

Theorem 3ad2antr1 1203
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 727 . 2 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
323adantr3 1186 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1099
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 209  df-an 400  df-3an 1101
This theorem is referenced by:  simpr1  1209  simpr1l  1245  simpr1r  1246  simpr11  1272  simpr12  1273  simpr13  1274  ispod  5565  funcnvqp  6586  dfwe2  7758  poxp  8109  cfcoflem  10230  axdc3lem  10408  fzadd2  13565  fzosubel2  13732  hashdifpr  14429  pfxccat3a  14752  sqrt0  15269  iscatd2  17714  funcestrcsetclem9  18181  funcsetcestrclem9  18196  curf2cl  18264  yonedalem4c  18310  grpsubadd  19071  mulgnnass  19152  mulgnn0ass  19153  dprdss  20072  dprd2da  20085  srgdilem  20243  lsssn0  21016  zntoslem  21609  sraassab  21921  blsscls  24568  iimulcl  25000  pi1grplem  25112  pi1xfrf  25116  dvconst  25980  logexprlim  27290  wwlksnextbi  30095  clwwlkccatlem  30192  clwwlkccat  30193  umgr3cyclex  30386  nvss  30797  disjdsct  32906  idlsrgmnd  33711  issgon  34421  measdivcst  34522  measdivcstALTV  34523  prv1n  35782  elmrsubrn  35871  poimirlem28  38148  ftc1anc  38201  fdc  38245  cvrnbtwn3  39901  paddasslem9  40453  paddasslem17  40461  pmapjlln1  40480  lautj  40718  lautm  40719  dfsalgen2  46916  smflimlem4  47349  lidldomnnring  48859  funcringcsetcALTV2lem9  48921  funcringcsetclem9ALTV  48944  lincresunit3lem2  49103  isthincd2  50059
  Copyright terms: Public domain W3C validator