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

Theorem sylancom 420
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 110 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 411 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  ordin  4403  fimacnvdisj  5419  fvimacnv  5651  ssct  6843  f1vrnfibi  6973  inl11  7093  ctssdc  7141  enomnilem  7165  enmkvlem  7188  djuen  7239  cauappcvgprlemlol  7675  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  caucvgprlemlol  7698  caucvgprlemladdrl  7706  caucvgprprlemlol  7726  suplocsrlem  7836  recgt1i  8884  avgle2  9189  xnn0le2is012  9895  ioodisj  10022  fzneuz  10130  fihashfn  10811  shftfvalg  10858  shftfval  10861  cvg1nlemres  11025  resqrexlem1arp  11045  maxabslemval  11248  xrmaxiflemval  11289  xrmaxadd  11300  xrminmax  11304  summodclem3  11419  fsumsplit  11446  mertenslemub  11573  fprodsplit  11636  demoivreALT  11812  zsupcllemstep  11977  gcdneg  12014  bezoutlemsup  12041  eucalginv  12087  eucalg  12090  odzdvds  12276  pclemdc  12319  fldivp1  12379  prmunb  12393  enctlem  12482  ctiunctlemfo  12489  intopsn  12840  grpsubval  12987  mulgnndir  13088  iscnp4  14170  cnntr  14177  tx2cn  14222  hmeontr  14265  hmeores  14267  xmetres2  14331  metres2  14333  limccnp2cntop  14598  limccoap  14599  isomninnlem  15232  iswomninnlem  15251  ismkvnnlem  15254
  Copyright terms: Public domain W3C validator