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

Theorem 3ad2antr1 1188
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 1171 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  simpr1  1194  simpr1l  1230  simpr1r  1231  simpr11  1257  simpr12  1258  simpr13  1259  ispod  5552  funcnvqp  6562  dfwe2  7700  poxp  8052  cfcoflem  10166  axdc3lem  10344  fzadd2  13430  fzosubel2  13586  hashdifpr  14269  pfxccat3a  14580  sqrt0  15080  iscatd2  17515  funcestrcsetclem9  17990  funcsetcestrclem9  18005  curf2cl  18074  yonedalem4c  18120  grpsubadd  18788  mulgnnass  18864  mulgnn0ass  18865  dprdss  19761  dprd2da  19774  srgdilem  19876  lsssn0  20355  zntoslem  20910  psrbaglesuppOLD  21274  blsscls  23809  iimulcl  24246  pi1grplem  24358  pi1xfrf  24362  dvconst  25227  logexprlim  26519  wwlksnextbi  28684  clwwlkccatlem  28778  clwwlkccat  28779  umgr3cyclex  28972  nvss  29380  disjdsct  31459  idlsrgmnd  32094  issgon  32550  measdivcst  32651  measdivcstALTV  32652  prv1n  33853  elmrsubrn  33942  poimirlem28  36038  ftc1anc  36091  fdc  36136  cvrnbtwn3  37670  paddasslem9  38223  paddasslem17  38231  pmapjlln1  38250  lautj  38488  lautm  38489  dfsalgen2  44477  smflimlem4  44910  lidldomnnring  46123  funcringcsetcALTV2lem9  46237  funcringcsetclem9ALTV  46260  lincresunit3lem2  46456  isthincd2  46953
  Copyright terms: Public domain W3C validator