ILE Home 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  842  con4biddc  852  jaddc  859  con1biddc  871  necon4addc  2410  necon4bddc  2411  necon4ddc  2412  necon1addc  2416  necon1bddc  2417  dmcosseq  4880  iss  4935  funopg  5230  snon0  6911  metrest  13265
  Copyright terms: Public domain W3C validator