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

Theorem syl5com 26
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1 (φψ)
syl5com.2 (χ → (ψθ))
Assertion
Ref Expression
syl5com (φ → (χθ))

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3 (φψ)
21a1d 22 . 2 (φ → (χψ))
3 syl5com.2 . 2 (χ → (ψθ))
42, 3sylcom 25 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:  com12  27  syl5  28  pm2.6dc  758  pm5.11dc  814  ax16i  1735  mor  1939  ceqsalg  2576  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  spc2egv  2636  spc2gv  2637  spc3egv  2638  spc3gv  2639  disjne  3267  uneqdifeqim  3302  triun  3858  sucssel  4127  ordsucg  4194  regexmidlem1  4218  relresfld  4790  relcoi1  4792  fornex  5684  f1dmex  5685  rdgon  5913  dom2d  6189  nneo  8117  zeo2  8120  uznfz  8735  difelfzle  8762  ssfzo12  8850  bj-indsuc  9383  bj-nntrans  9405
  Copyright terms: Public domain W3C validator