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

Theorem syl21anc 1134
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  4056  brcogw  4504  funprg  4949  funtpg  4950  fnunsn  5006  ftpg  5347  fsnunf  5362  isotr  5456  off  5724  caofrss  5735  ac6sfi  6352  mulclpi  6424  archnqq  6513  addlocprlemlt  6627  addlocprlemeq  6629  addlocprlemgt  6630  mullocprlem  6666  apreim  7592  ltrec1  7852  divge0d  8661  fseq1p1m1  8954  iseqcaopr2  9215  iseqdistr  9223  shftfibg  9395  sqrtdiv  9614  sqrtdivd  9738  mulcn2  9806
  Copyright terms: Public domain W3C validator