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

Theorem syl2anr 274
Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
Hypotheses
Ref Expression
syl2an.1
syl2an.2
syl2an.3
Assertion
Ref Expression
syl2anr

Proof of Theorem syl2anr
StepHypRef Expression
1 syl2an.1 . . 3
2 syl2an.2 . . 3
3 syl2an.3 . . 3
41, 2, 3syl2an 273 . 2
54ancoms 255 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-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  swopo  4034  opswapg  4750  coexg  4805  iotass  4827  resdif  5091  fvexg  5137  isotr  5399  xpexgALT  5702  cauappcvgprlemladdfl  6626  addgt0sr  6683  axmulass  6737  axdistr  6738  negeu  6979  nnsub  7713  zltnle  8047  elz2  8068  uzaddcl  8285  qaddcl  8326  xltneg  8499  xleneg  8500  iccneg  8607  uzsubsubfz  8661  fzsplit2  8664  fzss1  8676  uzsplit  8704  fz0fzdiffz0  8737  difelfzle  8742  difelfznle  8743  fzonlt0  8773  fzouzsplit  8785  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  ssfzo12  8830  nn0ennn  8870  crim  9066
  Copyright terms: Public domain W3C validator