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

Theorem 3ad2antr1 1189
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 716 . 2 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
323adantr3 1172 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  simpr1  1195  simpr1l  1231  simpr1r  1232  simpr11  1258  simpr12  1259  simpr13  1260  ispod  5555  funcnvqp  6566  dfwe2  7709  poxp  8061  cfcoflem  10209  axdc3lem  10387  fzadd2  13477  fzosubel2  13633  hashdifpr  14316  pfxccat3a  14627  sqrt0  15127  iscatd2  17562  funcestrcsetclem9  18037  funcsetcestrclem9  18052  curf2cl  18121  yonedalem4c  18167  grpsubadd  18836  mulgnnass  18912  mulgnn0ass  18913  dprdss  19809  dprd2da  19822  srgdilem  19924  lsssn0  20411  zntoslem  20966  psrbaglesuppOLD  21330  blsscls  23866  iimulcl  24303  pi1grplem  24415  pi1xfrf  24419  dvconst  25284  logexprlim  26576  wwlksnextbi  28842  clwwlkccatlem  28936  clwwlkccat  28937  umgr3cyclex  29130  nvss  29538  disjdsct  31619  idlsrgmnd  32259  issgon  32725  measdivcst  32826  measdivcstALTV  32827  prv1n  34028  elmrsubrn  34117  poimirlem28  36109  ftc1anc  36162  fdc  36207  cvrnbtwn3  37741  paddasslem9  38294  paddasslem17  38302  pmapjlln1  38321  lautj  38559  lautm  38560  dfsalgen2  44589  smflimlem4  45022  lidldomnnring  46235  funcringcsetcALTV2lem9  46349  funcringcsetclem9ALTV  46372  lincresunit3lem2  46568  isthincd2  47065
  Copyright terms: Public domain W3C validator