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

Theorem sylancom 418
Description: Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)
Hypotheses
Ref Expression
sylancom.1 ((𝜑𝜓) → 𝜒)
sylancom.2 ((𝜒𝜓) → 𝜃)
Assertion
Ref Expression
sylancom ((𝜑𝜓) → 𝜃)

Proof of Theorem sylancom
StepHypRef Expression
1 sylancom.1 . 2 ((𝜑𝜓) → 𝜒)
2 simpr 109 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 409 1 ((𝜑𝜓) → 𝜃)
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  4368  fimacnvdisj  5380  fvimacnv  5608  ssct  6792  f1vrnfibi  6918  inl11  7038  ctssdc  7086  enomnilem  7110  enmkvlem  7133  djuen  7175  cauappcvgprlemlol  7596  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  caucvgprlemlol  7619  caucvgprlemladdrl  7627  caucvgprprlemlol  7647  suplocsrlem  7757  recgt1i  8801  avgle2  9106  xnn0le2is012  9810  ioodisj  9937  fzneuz  10044  fihashfn  10722  shftfvalg  10769  shftfval  10772  cvg1nlemres  10936  resqrexlem1arp  10956  maxabslemval  11159  xrmaxiflemval  11200  xrmaxadd  11211  xrminmax  11215  summodclem3  11330  fsumsplit  11357  mertenslemub  11484  fprodsplit  11547  demoivreALT  11723  zsupcllemstep  11887  gcdsupex  11899  gcdsupcl  11900  gcdneg  11924  bezoutlemsup  11951  eucalginv  11997  eucalg  12000  odzdvds  12186  fldivp1  12287  prmunb  12301  enctlem  12374  ctiunctlemfo  12381  intopsn  12608  iscnp4  12971  cnntr  12978  tx2cn  13023  hmeontr  13066  hmeores  13068  xmetres2  13132  metres2  13134  limccnp2cntop  13399  limccoap  13400  isomninnlem  14022  iswomninnlem  14041  ismkvnnlem  14044
  Copyright terms: Public domain W3C validator