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

Theorem sylanr1 681
 Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.)
Hypotheses
Ref Expression
sylanr1.1 (𝜑𝜒)
sylanr1.2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
sylanr1 ((𝜓 ∧ (𝜑𝜃)) → 𝜏)

Proof of Theorem sylanr1
StepHypRef Expression
1 sylanr1.1 . . 3 (𝜑𝜒)
21anim1i 617 . 2 ((𝜑𝜃) → (𝜒𝜃))
3 sylanr1.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 595 1 ((𝜓 ∧ (𝜑𝜃)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  adantrll  721  adantrlr  722  sbthlem9  8632  pczpre  16182  cpmadugsumlemF  21487  blsscls2  23117  rpvmasumlem  26077  leopmuli  29922  chirredlem1  30179  chirredlem3  30181  pibt2  34782  dvconstbi  40962  bccbc  40973  reccot  45214  rectan  45215  aacllem  45259
 Copyright terms: Public domain W3C validator