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

Theorem 3ad2antr2 1240
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 707 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1212 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  simpr2  1250  simpr2l  1309  simpr2r  1311  simpr21  1353  simpr22  1355  simpr23  1357  wereu  5275  axdc4lem  9534  ioc0  12429  funcestrcsetclem9  17068  funcsetcestrclem9  17083  grpsubadd  17784  psrbaglesupp  19656  zntoslem  20191  trcfilu  22391  mdsl3  29652  dvrcan5  30261  brofs2  32649  brifs2  32650  poimirlem28  33882  ftc1anc  33937  frinfm  33974  welb  33975  fdc  33984  unichnidl  34273  cvrnbtwn2  35252  islpln2a  35525  paddss1  35794  paddss2  35795  paddasslem17  35813  tendospass  36996  funcringcsetcALTV2lem9  42737  funcringcsetclem9ALTV  42760  ldepsprlem  42954
  Copyright terms: Public domain W3C validator