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

Theorem syl5com 29
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1  |-  ( ph  ->  ps )
syl5com.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5com  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3  |-  ( ph  ->  ps )
21a1d 22 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
3 syl5com.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3sylcom 28 1  |-  ( ph  ->  ( ch  ->  th )
)
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:  com12  30  syl5  32  pm2.6dc  862  pm5.11dc  909  ax16i  1858  mor  2068  ceqsalg  2765  cgsexg  2772  cgsex2g  2773  cgsex4g  2774  spc2egv  2827  spc2gv  2828  spc3egv  2829  spc3gv  2830  disjne  3476  uneqdifeqim  3508  eqifdc  3569  triun  4114  sucssel  4424  ordsucg  4501  regexmidlem1  4532  relresfld  5158  relcoi1  5160  focdmex  6115  f1dmex  6116  dom2d  6772  findcard  6887  nneo  9354  zeo2  9357  uznfz  10100  difelfzle  10131  ssfzo12  10221  facndiv  10714  fisumcom2  11441  fprodssdc  11593  fprodcom2fi  11629  ndvdssub  11929  bezoutlembi  12000  eucalglt  12051  prmind2  12114  coprm  12138  prmdiveq  12230  mhmlin  12812  issubg2m  13002  nsgbi  13017  issubrg2  13322  inopn  13394  basis1  13438  tgss  13456  tgcl  13457  xmeteq0  13752  blssexps  13822  blssex  13823  mopni3  13877  neibl  13884  metss  13887  metcnp3  13904  logbgcd1irr  14278  bj-indsuc  14562  bj-nntrans  14585
  Copyright terms: Public domain W3C validator