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

Theorem sylcom 25
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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl5com  26  syl6  29  syli  33  mpbidi  140  con4biddc  753  jaddc  760  con1biddc  769  necon4addc  2269  necon4bddc  2270  necon4ddc  2271  necon1addc  2275  necon1bddc  2276  dmcosseq  4546  iss  4597  funopg  4877
  Copyright terms: Public domain W3C validator