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

Theorem sylancom 411
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 108 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 403 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ordin  4175  fimacnvdisj  5142  fvimacnv  5358  ssct  6463  f1vrnfibi  6578  enomnilem  6698  cauappcvgprlemlol  7108  cauappcvgprlemladdru  7117  cauappcvgprlemladdrl  7118  caucvgprlemlol  7131  caucvgprlemladdrl  7139  caucvgprprlemlol  7159  recgt1i  8252  avgle2  8548  ioodisj  9304  fzneuz  9407  fihashfn  10042  shftfvalg  10079  shftfval  10082  cvg1nlemres  10244  resqrexlem1arp  10264  maxabslemval  10467  zsupcllemstep  10720  gcdsupex  10728  gcdsupcl  10729  gcdneg  10752  bezoutlemsup  10777  eucalginv  10817  eucialg  10820
  Copyright terms: Public domain W3C validator