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  6426  archnqq  6515  addlocprlemlt  6629  addlocprlemeq  6631  addlocprlemgt  6632  mullocprlem  6668  apreim  7594  ltrec1  7854  divge0d  8663  fseq1p1m1  8956  iseqcaopr2  9241  iseqdistr  9249  shftfibg  9421  sqrtdiv  9640  sqrtdivd  9764  mulcn2  9833
 Copyright terms: Public domain W3C validator