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

Theorem syl5com 29
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 28 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  30  syl5  32  pm2.6dc  797  pm5.11dc  853  ax16i  1786  mor  1990  ceqsalg  2647  cgsexg  2654  cgsex2g  2655  cgsex4g  2656  spc2egv  2708  spc2gv  2709  spc3egv  2710  spc3gv  2711  disjne  3333  uneqdifeqim  3364  eqifdc  3421  triun  3941  sucssel  4242  ordsucg  4309  regexmidlem1  4339  relresfld  4947  relcoi1  4949  fornex  5868  f1dmex  5869  dom2d  6470  findcard  6584  nneo  8819  zeo2  8822  uznfz  9484  difelfzle  9510  ssfzo12  9600  facndiv  10112  fisumcom2  10795  ndvdssub  11023  bezoutlembi  11087  eucalglt  11132  prmind2  11195  coprm  11216  bj-indsuc  11480  bj-nntrans  11503
  Copyright terms: Public domain W3C validator