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

Theorem sylan9 406
 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 72 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43imp 123 1 ((𝜑𝜃) → (𝜓𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106 This theorem is referenced by:  sbequi  1811  rspc2  2800  rspc3v  2805  copsexg  4166  chfnrn  5531  ffnfv  5578  f1elima  5674  smoel2  6200  th3q  6534  fiintim  6817  addnnnq0  7271  mulnnnq0  7272  addsrpr  7567  mulsrpr  7568  cau3lem  10900  rescncf  12753
 Copyright terms: Public domain W3C validator