Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anr 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  4043  opswapg  4807  coexg  4862  iotass  4884  resdif  5148  fvexg  5194  isotr  5456  xpexgALT  5760  cauappcvgprlemladdfl  6753  addgt0sr  6860  axmulass  6947  axdistr  6948  negeu  7202  nnsub  7952  zltnle  8291  elz2  8312  uzaddcl  8529  qaddcl  8570  xltneg  8749  xleneg  8750  iccneg  8857  uzsubsubfz  8911  fzsplit2  8914  fzss1  8926  uzsplit  8954  fz0fzdiffz0  8987  difelfzle  8992  difelfznle  8993  fzonlt0  9023  fzouzsplit  9035  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  ssfzo12  9080  qltnle  9101  nn0ennn  9209  isermono  9237  crim  9458  nn0seqcvgd  9880  algcvgblem  9888
 Copyright terms: Public domain W3C validator