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

Theorem sylanr1 682
 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 590 . 2 ((𝜑𝜃) → (𝜒𝜃))
3 sylanr1.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 490 1 ((𝜓 ∧ (𝜑𝜃)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 This theorem is referenced by:  adantrll  754  adantrlr  755  sbthlem9  7963  pczpre  15390  cpmadugsumlemF  20500  blsscls2  22119  rpvmasumlem  24976  leopmuli  28376  chirredlem1  28633  chirredlem3  28635  dvconstbi  37555  bccbc  37566  reccot  42298  rectan  42299  aacllem  42356
 Copyright terms: Public domain W3C validator