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

Theorem syl21anc 1145
 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 296 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anc.4 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
64, 5syl 14 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-ia3 105 This theorem is referenced by:  issod  4084  brcogw  4532  funprg  4977  funtpg  4978  fnunsn  5034  ftpg  5375  fsnunf  5390  isotr  5484  off  5752  caofrss  5763  ac6sfi  6383  mulclpi  6484  archnqq  6573  addlocprlemlt  6687  addlocprlemeq  6689  addlocprlemgt  6690  mullocprlem  6726  apreim  7668  ltrec1  7929  divge0d  8761  fseq1p1m1  9058  q2submod  9335  iseqcaopr2  9405  iseqdistr  9414  facavg  9614  shftfibg  9649  sqrtdiv  9869  sqrtdivd  9995  mulcn2  10064  oddpwdclemodd  10260
 Copyright terms: Public domain W3C validator