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

Theorem sylancom 414
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 406 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ordin  4265  fimacnvdisj  5263  fvimacnv  5487  ssct  6663  f1vrnfibi  6783  inl11  6900  ctssdc  6948  enomnilem  6958  djuen  7012  cauappcvgprlemlol  7397  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  caucvgprlemlol  7420  caucvgprlemladdrl  7428  caucvgprprlemlol  7448  recgt1i  8560  avgle2  8859  xnn0le2is012  9536  ioodisj  9663  fzneuz  9768  fihashfn  10433  shftfvalg  10477  shftfval  10480  cvg1nlemres  10643  resqrexlem1arp  10663  maxabslemval  10866  xrmaxiflemval  10905  xrmaxadd  10916  xrminmax  10920  summodclem3  11035  fsumsplit  11062  mertenslemub  11189  demoivreALT  11324  zsupcllemstep  11480  gcdsupex  11488  gcdsupcl  11489  gcdneg  11512  bezoutlemsup  11537  eucalginv  11577  eucalg  11580  ctiunctlemfo  11789  iscnp4  12223  cnntr  12230  tx2cn  12275  xmetres2  12362  metres2  12364  limccnp2cntop  12596  isomninnlem  12906
  Copyright terms: Public domain W3C validator