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

Theorem sylancom 417
 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  4316  fimacnvdisj  5316  fvimacnv  5544  ssct  6721  f1vrnfibi  6843  inl11  6960  ctssdc  7008  enomnilem  7020  enmkvlem  7045  djuen  7087  cauappcvgprlemlol  7499  cauappcvgprlemladdru  7508  cauappcvgprlemladdrl  7509  caucvgprlemlol  7522  caucvgprlemladdrl  7530  caucvgprprlemlol  7550  suplocsrlem  7660  recgt1i  8700  avgle2  9005  xnn0le2is012  9699  ioodisj  9826  fzneuz  9932  fihashfn  10598  shftfvalg  10642  shftfval  10645  cvg1nlemres  10809  resqrexlem1arp  10829  maxabslemval  11032  xrmaxiflemval  11071  xrmaxadd  11082  xrminmax  11086  summodclem3  11201  fsumsplit  11228  mertenslemub  11355  demoivreALT  11536  zsupcllemstep  11694  gcdsupex  11702  gcdsupcl  11703  gcdneg  11726  bezoutlemsup  11753  eucalginv  11793  eucalg  11796  enctlem  12001  ctiunctlemfo  12008  iscnp4  12446  cnntr  12453  tx2cn  12498  hmeontr  12541  hmeores  12543  xmetres2  12607  metres2  12609  limccnp2cntop  12874  limccoap  12875  isomninnlem  13419  iswomninnlem  13438  ismkvnnlem  13441
 Copyright terms: Public domain W3C validator