Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan9 GIF version

Theorem sylan9 395
 Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
sylan9.1 (𝜑 → (𝜓𝜒))
sylan9.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9 ((𝜑𝜃) → (𝜓𝜏))

Proof of Theorem sylan9
StepHypRef Expression
1 sylan9.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan9.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2syl9 70 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43imp 119 1 ((𝜑𝜃) → (𝜓𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104 This theorem is referenced by:  sbequi  1736  rspc2  2683  rspc3v  2688  trintssmOLD  3899  copsexg  4009  chfnrn  5306  ffnfv  5351  f1elima  5440  smoel2  5949  th3q  6242  addnnnq0  6605  mulnnnq0  6606  addsrpr  6888  mulsrpr  6889  cau3lem  9941
 Copyright terms: Public domain W3C validator