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  793  pm5.11dc  849  ax16i  1781  mor  1985  ceqsalg  2636  cgsexg  2643  cgsex2g  2644  cgsex4g  2645  spc2egv  2696  spc2gv  2697  spc3egv  2698  spc3gv  2699  disjne  3313  uneqdifeqim  3344  triun  3908  sucssel  4207  ordsucg  4274  regexmidlem1  4304  relresfld  4897  relcoi1  4899  fornex  5793  f1dmex  5794  dom2d  6341  findcard  6444  nneo  8583  zeo2  8586  uznfz  9248  difelfzle  9274  ssfzo12  9362  facndiv  9815  ndvdssub  10537  bezoutlembi  10601  eucalglt  10646  prmind2  10709  coprm  10730  bj-indsuc  10990  bj-nntrans  11013
 Copyright terms: Public domain W3C validator