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

Theorem sylanr1 653
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 594 . 2 ((𝜑𝜃) → (𝜒𝜃))
3 sylanr1.2 . 2 ((𝜓 ∧ (𝜒𝜃)) → 𝜏)
42, 3sylan2 572 1 ((𝜓 ∧ (𝜑𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  adantrll  693  adantrlr  694  sbthlem9  8233  pczpre  15758  cpmadugsumlemF  20900  blsscls2  22528  rpvmasumlem  25396  leopmuli  29326  chirredlem1  29583  chirredlem3  29585  dvconstbi  39052  bccbc  39063  reccot  43020  rectan  43021  aacllem  43068
  Copyright terms: Public domain W3C validator