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

Theorem sylancom 397
 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 103 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 391 1 ((𝜑𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101 This theorem is referenced by:  ordin  4122  fimacnvdisj  5074  fvimacnv  5282  cauappcvgprlemlol  6745  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemlol  6768  caucvgprlemladdrl  6776  caucvgprprlemlol  6796  recgt1i  7864  avgle2  8166  ioodisj  8861  fzneuz  8963  shftfvalg  9419  shftfval  9422  cvg1nlemres  9584  resqrexlem1arp  9603
 Copyright terms: Public domain W3C validator