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  4046  brcogw  4446  funprg  4890  funtpg  4891  fnunsn  4947  ftpg  5288  fsnunf  5303  isotr  5397  off  5663  caofrss  5674  mulclpi  6305  archnqq  6393  addlocprlemlt  6507  addlocprlemeq  6509  addlocprlemgt  6510  mullocprlem  6541  apreim  7339  ltrec1  7586  divge0d  8381  fseq1p1m1  8672
  Copyright terms: Public domain W3C validator