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

Theorem syl21anc 1216
 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 307 . 2
5 syl21anc.4 . 2
64, 5syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107 This theorem is referenced by:  issod  4250  brcogw  4718  funprg  5183  funtpg  5184  fnunsn  5240  ftpg  5614  fsnunf  5630  isotr  5727  off  6004  caofrss  6016  tfr1onlembxssdm  6250  tfrcllembxssdm  6263  pmresg  6580  ac6sfi  6802  tridc  6803  fidcenumlemrks  6854  sbthlemi8  6865  casefun  6983  caseinj  6987  djufun  7002  djuinj  7004  mulclpi  7183  archnqq  7272  addlocprlemlt  7386  addlocprlemeq  7388  addlocprlemgt  7389  mullocprlem  7425  apreim  8412  subrecap  8645  ltrec1  8693  divge0d  9577  fseq1p1m1  9928  q2submod  10212  seq3caopr2  10309  seq3distr  10340  facavg  10547  shftfibg  10647  sqrtdiv  10869  sqrtdivd  10995  mulcn2  11136  demoivreALT  11539  dvdslegcd  11712  gcdnncl  11715  qredeu  11837  rpdvds  11839  rpexp  11890  oddpwdclemodd  11909  divnumden  11933  divdenle  11934  phimullem  11960  setsfun  12056  setsfun0  12057  strleund  12109  comet  12730  fsumcncntop  12787  mulcncf  12822  trilpo  13445  neapmkv  13469
 Copyright terms: Public domain W3C validator