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  832  pm5.11dc  879  ax16i  1814  mor  2019  ceqsalg  2688  cgsexg  2695  cgsex2g  2696  cgsex4g  2697  spc2egv  2749  spc2gv  2750  spc3egv  2751  spc3gv  2752  disjne  3386  uneqdifeqim  3418  eqifdc  3476  triun  4009  sucssel  4316  ordsucg  4388  regexmidlem1  4418  relresfld  5038  relcoi1  5040  fornex  5981  f1dmex  5982  dom2d  6635  findcard  6750  nneo  9122  zeo2  9125  uznfz  9851  difelfzle  9879  ssfzo12  9969  facndiv  10453  fisumcom2  11175  ndvdssub  11554  bezoutlembi  11620  eucalglt  11665  prmind2  11728  coprm  11749  inopn  12097  basis1  12141  tgss  12159  tgcl  12160  xmeteq0  12455  blssexps  12525  blssex  12526  mopni3  12580  neibl  12587  metss  12590  metcnp3  12607  bj-indsuc  13053  bj-nntrans  13076
  Copyright terms: Public domain W3C validator