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  4203  fimacnvdisj  5179  fvimacnv  5398  ssct  6514  f1vrnfibi  6633  enomnilem  6773  cauappcvgprlemlol  7185  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemlol  7208  caucvgprlemladdrl  7216  caucvgprprlemlol  7236  recgt1i  8331  avgle2  8627  ioodisj  9379  fzneuz  9482  fihashfn  10173  shftfvalg  10217  shftfval  10220  cvg1nlemres  10383  resqrexlem1arp  10403  maxabslemval  10606  isummolem3  10734  fsumsplit  10764  zsupcllemstep  11034  gcdsupex  11042  gcdsupcl  11043  gcdneg  11066  bezoutlemsup  11091  eucalginv  11131  eucialg  11134
  Copyright terms: Public domain W3C validator