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

Theorem sylcom 28
 Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)
Hypotheses
Ref Expression
sylcom.1 (𝜑 → (𝜓𝜒))
sylcom.2 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
sylcom (𝜑 → (𝜓𝜃))

Proof of Theorem sylcom
StepHypRef Expression
1 sylcom.1 . 2 (𝜑 → (𝜓𝜒))
2 sylcom.2 . . 3 (𝜓 → (𝜒𝜃))
32a2i 11 . 2 ((𝜓𝜒) → (𝜓𝜃))
41, 3syl 14 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  syl5com  29  syl6  33  syli  37  mpbidi  150  stdcn  832  con4biddc  842  jaddc  849  con1biddc  861  necon4addc  2378  necon4bddc  2379  necon4ddc  2380  necon1addc  2384  necon1bddc  2385  dmcosseq  4810  iss  4865  funopg  5157  snon0  6824  metrest  12685
 Copyright terms: Public domain W3C validator