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

Theorem 3ad2antr2 1247
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 752 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1242 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  wereu  5139  axdc4lem  9315  ioc0  12260  funcestrcsetclem9  16835  funcsetcestrclem9  16850  grpsubadd  17550  psrbaglesupp  19416  zntoslem  19953  trcfilu  22145  mdsl3  29303  dvrcan5  29921  brofs2  32309  brifs2  32310  poimirlem28  33567  ftc1anc  33623  frinfm  33660  welb  33661  fdc  33671  unichnidl  33960  cvrnbtwn2  34880  islpln2a  35152  paddss1  35421  paddss2  35422  paddasslem17  35440  tendospass  36625  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  ldepsprlem  42586
  Copyright terms: Public domain W3C validator