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

Theorem 3ad2antr1 1185
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 715 . 2 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
323adantr3 1168 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  simpr1  1191  simpr1l  1227  simpr1r  1228  simpr11  1254  simpr12  1255  simpr13  1256  ispod  5603  funcnvqp  6623  dfwe2  7782  poxp  8142  cfcoflem  10315  axdc3lem  10493  fzadd2  13590  fzosubel2  13746  hashdifpr  14432  pfxccat3a  14746  sqrt0  15246  iscatd2  17694  funcestrcsetclem9  18172  funcsetcestrclem9  18187  curf2cl  18256  yonedalem4c  18302  grpsubadd  19022  mulgnnass  19103  mulgnn0ass  19104  dprdss  20029  dprd2da  20042  srgdilem  20175  lsssn0  20925  zntoslem  21554  sraassab  21865  psrbaglesuppOLD  21922  blsscls  24507  iimulcl  24951  pi1grplem  25067  pi1xfrf  25071  dvconst  25937  logexprlim  27254  wwlksnextbi  29828  clwwlkccatlem  29922  clwwlkccat  29923  umgr3cyclex  30116  nvss  30526  disjdsct  32614  idlsrgmnd  33389  issgon  33956  measdivcst  34057  measdivcstALTV  34058  prv1n  35259  elmrsubrn  35348  poimirlem28  37349  ftc1anc  37402  fdc  37446  cvrnbtwn3  38974  paddasslem9  39527  paddasslem17  39535  pmapjlln1  39554  lautj  39792  lautm  39793  dfsalgen2  45962  smflimlem4  46395  lidldomnnring  47613  funcringcsetcALTV2lem9  47675  funcringcsetclem9ALTV  47698  lincresunit3lem2  47863  isthincd2  48359
  Copyright terms: Public domain W3C validator