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

Theorem 3ad2antr1 1219
 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 749 . 2 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
323adantr3 1215 1 ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  ispod  4967  funcnvqp  5866  dfwe2  6873  poxp  7176  cfcoflem  8977  axdc3lem  9155  fzadd2  12247  fzosubel2  12395  hashdifpr  13064  sqr0lem  13829  iscatd2  16165  funcestrcsetclem9  16611  funcsetcestrclem9  16626  curf2cl  16694  yonedalem4c  16740  grpsubadd  17326  mulgnnass  17399  mulgnnassOLD  17400  mulgnn0ass  17401  dprdss  18251  dprd2da  18264  srgi  18334  lsssn0  18769  psrbaglesupp  19189  zntoslem  19724  blsscls  22122  iimulcl  22544  pi1grplem  22657  pi1xfrf  22661  dvconst  23486  logexprlim  24750  constr3trllem1  26178  wwlknextbi  26253  nvss  26832  disjdsct  28863  issgon  29513  measdivcstOLD  29614  measdivcst  29615  elmrsubrn  30671  poimirlem28  32607  ftc1anc  32663  fdc  32711  cvrnbtwn3  33581  paddasslem9  34132  paddasslem17  34140  pmapjlln1  34159  lautj  34397  lautm  34398  dfsalgen2  39235  smflimlem4  39660  pfxccat3a  40292  splvalpfx  40298  wwlksnextbi  41100  umgr3cyclex  41350  lidldomnnring  41720  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  lincresunit3lem2  42063
 Copyright terms: Public domain W3C validator