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

Theorem 3ad2antr2 1183
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antr2 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)

Proof of Theorem 3ad2antr2
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantrl 712 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1165 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  simpr2  1189  simpr2l  1226  simpr2r  1227  simpr21  1254  simpr22  1255  simpr23  1256  wereu  5550  axdc4lem  9871  ioc0  12780  funcestrcsetclem9  17393  funcsetcestrclem9  17408  grpsubadd  18132  psrbaglesupp  20083  zntoslem  20638  mdsl3  30026  dvrcan5  30797  prv1n  32581  brofs2  33441  brifs2  33442  poimirlem28  34806  ftc1anc  34861  frinfm  34897  welb  34898  fdc  34907  unichnidl  35196  cvrnbtwn2  36297  islpln2a  36570  paddss1  36839  paddss2  36840  paddasslem17  36858  tendospass  38041  funcringcsetcALTV2lem9  44217  funcringcsetclem9ALTV  44240  ldepsprlem  44429
  Copyright terms: Public domain W3C validator