MPE Home 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  7941  pczpre  15339  cpmadugsumlemF  20448  blsscls2  22067  rpvmasumlem  24921  leopmuli  28170  chirredlem1  28427  chirredlem3  28429  dvconstbi  37349  bccbc  37360  reccot  42251  rectan  42252  aacllem  42309
  Copyright terms: Public domain W3C validator