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  4186  fimacnvdisj  5158  fvimacnv  5377  ssct  6486  f1vrnfibi  6604  enomnilem  6738  cauappcvgprlemlol  7150  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemlol  7173  caucvgprlemladdrl  7181  caucvgprprlemlol  7201  recgt1i  8294  avgle2  8590  ioodisj  9342  fzneuz  9445  fihashfn  10104  shftfvalg  10148  shftfval  10151  cvg1nlemres  10313  resqrexlem1arp  10333  maxabslemval  10536  isummolem3  10659  zsupcllemstep  10816  gcdsupex  10824  gcdsupcl  10825  gcdneg  10848  bezoutlemsup  10873  eucalginv  10913  eucialg  10916
  Copyright terms: Public domain W3C validator