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

Theorem sylancom 405
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 107 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 397 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ordin  4149  fimacnvdisj  5101  fvimacnv  5309  cauappcvgprlemlol  6802  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  caucvgprlemlol  6825  caucvgprlemladdrl  6833  caucvgprprlemlol  6853  recgt1i  7938  avgle2  8222  ioodisj  8961  fzneuz  9064  shftfvalg  9646  shftfval  9649  cvg1nlemres  9811  resqrexlem1arp  9831
  Copyright terms: Public domain W3C validator