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

Theorem sylancom 417
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 109 . 2  |-  ( (
ph  /\  ps )  ->  ps )
3 sylancom.2 . 2  |-  ( ( ch  /\  ps )  ->  th )
41, 2, 3syl2anc 409 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ordin  4311  fimacnvdisj  5311  fvimacnv  5539  ssct  6716  f1vrnfibi  6837  inl11  6954  ctssdc  7002  enomnilem  7014  enmkvlem  7039  djuen  7080  cauappcvgprlemlol  7475  cauappcvgprlemladdru  7484  cauappcvgprlemladdrl  7485  caucvgprlemlol  7498  caucvgprlemladdrl  7506  caucvgprprlemlol  7526  suplocsrlem  7636  recgt1i  8676  avgle2  8981  xnn0le2is012  9675  ioodisj  9802  fzneuz  9908  fihashfn  10574  shftfvalg  10618  shftfval  10621  cvg1nlemres  10785  resqrexlem1arp  10805  maxabslemval  11008  xrmaxiflemval  11047  xrmaxadd  11058  xrminmax  11062  summodclem3  11177  fsumsplit  11204  mertenslemub  11331  demoivreALT  11507  zsupcllemstep  11665  gcdsupex  11673  gcdsupcl  11674  gcdneg  11697  bezoutlemsup  11724  eucalginv  11764  eucalg  11767  enctlem  11972  ctiunctlemfo  11979  iscnp4  12417  cnntr  12424  tx2cn  12469  hmeontr  12512  hmeores  12514  xmetres2  12578  metres2  12580  limccnp2cntop  12845  limccoap  12846  isomninnlem  13383  iswomninnlem  13400  ismkvnnlem  13402
  Copyright terms: Public domain W3C validator