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

Theorem sylancom 411
Description: Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)
Hypotheses
Ref Expression
sylancom.1  |-  ( (
ph  /\  ps )  ->  ch )
sylancom.2  |-  ( ( ch  /\  ps )  ->  th )
Assertion
Ref Expression
sylancom  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem sylancom
StepHypRef Expression
1 sylancom.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 simpr 108 . 2  |-  ( (
ph  /\  ps )  ->  ps )
3 sylancom.2 . 2  |-  ( ( ch  /\  ps )  ->  th )
41, 2, 3syl2anc 403 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ordin  4142  fimacnvdisj  5099  fvimacnv  5308  f1vrnfibi  6443  cauappcvgprlemlol  6888  cauappcvgprlemladdru  6897  cauappcvgprlemladdrl  6898  caucvgprlemlol  6911  caucvgprlemladdrl  6919  caucvgprprlemlol  6939  recgt1i  8032  avgle2  8328  ioodisj  9080  fzneuz  9183  sizefn  9813  shftfvalg  9833  shftfval  9836  cvg1nlemres  9998  resqrexlem1arp  10018  maxabslemval  10221  zsupcllemstep  10474  gcdsupex  10482  gcdsupcl  10483  gcdneg  10506  bezoutlemsup  10531  eucalginv  10571  eucialg  10574
  Copyright terms: Public domain W3C validator