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

Theorem syl112anc 1138
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
syl112anc.5
Assertion
Ref Expression
syl112anc

Proof of Theorem syl112anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . . 3
4 sylXanc.4 . . 3
53, 4jca 290 . 2
6 syl112anc.5 . 2
71, 2, 5, 6syl3anc 1134 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  fvun1  5182  reapmul1  7379  recrecap  7467  rec11rap  7469  divdivdivap  7471  dmdcanap  7480  ddcanap  7484  rerecclap  7488  div2negap  7493  divap1d  7558  divmulapd  7569  divmulap2d  7580  divmulap3d  7581  divassapd  7582  div12apd  7583  div23apd  7584  divdirapd  7585  divsubdirapd  7586  div11apd  7587  ltmul12a  7607  ltdiv1  7615  ltrec  7630  lt2msq1  7632  lediv2  7638  lediv23  7640  recp1lt1  7646  qapne  8350  expgt1  8947  nnlesq  9009  expnbnd  9025
  Copyright terms: Public domain W3C validator