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

Theorem sylan9 389
 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 66 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43imp 115 1 ((𝜑𝜃) → (𝜓𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100 This theorem is referenced by:  sbequi  1720  rspc2  2661  rspc3v  2665  trintssm  3870  copsexg  3981  chfnrn  5278  ffnfv  5323  f1elima  5412  smoel2  5918  th3q  6211  addnnnq0  6547  mulnnnq0  6548  addsrpr  6830  mulsrpr  6831  cau3lem  9710
 Copyright terms: Public domain W3C validator