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

Theorem 3ad2antr2 1220
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 748 . 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:  wereu  5024  axdc4lem  9138  ioc0  12052  funcestrcsetclem9  16560  funcsetcestrclem9  16575  grpsubadd  17275  psrbaglesupp  19138  zntoslem  19672  trcfilu  21856  constr2wlk  25922  constr2trl  25923  constr3trllem1  25972  mdsl3  28353  dvrcan5  28918  brofs2  31148  brifs2  31149  poimirlem28  32401  ftc1anc  32457  frinfm  32494  welb  32495  fdc  32505  unichnidl  32794  cvrnbtwn2  33374  islpln2a  33646  paddss1  33915  paddss2  33916  paddasslem17  33934  tendospass  35120  funcringcsetcALTV2lem9  41828  funcringcsetclem9ALTV  41851  ldepsprlem  42047
  Copyright terms: Public domain W3C validator