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

Theorem syl21anc 1133
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1 (φψ)
sylXanc.2 (φχ)
sylXanc.3 (φθ)
syl21anc.4 (((ψ χ) θ) → τ)
Assertion
Ref Expression
syl21anc (φτ)

Proof of Theorem syl21anc
StepHypRef Expression
1 sylXanc.1 . . 3 (φψ)
2 sylXanc.2 . . 3 (φχ)
3 sylXanc.3 . . 3 (φθ)
41, 2, 3jca31 292 . 2 (φ → ((ψ χ) θ))
5 syl21anc.4 . 2 (((ψ χ) θ) → τ)
64, 5syl 14 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-ia3 101
This theorem is referenced by:  issod  4047  brcogw  4447  funprg  4892  funtpg  4893  fnunsn  4949  ftpg  5290  fsnunf  5305  isotr  5399  off  5666  caofrss  5677  mulclpi  6312  archnqq  6400  addlocprlemlt  6513  addlocprlemeq  6515  addlocprlemgt  6516  mullocprlem  6550  apreim  7367  ltrec1  7615  divge0d  8413  fseq1p1m1  8706
  Copyright terms: Public domain W3C validator