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

Theorem syl2anr 286
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 285 . 2 ((𝜑𝜏) → 𝜃)
54ancoms 266 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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  swopo  4196  opswapg  4993  coexg  5051  iotass  5073  resdif  5355  fvexg  5406  isotr  5683  xpexgALT  5997  ixpssmapg  6588  mapen  6706  mapdom1g  6707  elfir  6827  cauappcvgprlemladdfl  7427  addgt0sr  7547  axmulass  7645  axdistr  7646  negeu  7917  ltaddnegr  8151  nnsub  8716  zltnle  9051  elz2  9073  uzaddcl  9330  qaddcl  9376  xltneg  9559  xleneg  9560  iccneg  9712  uzsubsubfz  9767  fzsplit2  9770  fzss1  9783  uzsplit  9812  fz0fzdiffz0  9847  difelfzle  9851  difelfznle  9852  fzonlt0  9884  fzouzsplit  9896  eluzgtdifelfzo  9914  elfzodifsumelfzo  9918  ssfzo12  9941  qltnle  9963  modfzo0difsn  10108  nn0ennn  10146  ser3mono  10191  iseqf1olemjpcl  10208  iseqf1olemqpcl  10209  fser0const  10229  faclbnd  10427  bcval4  10438  bcpasc  10452  hashfacen  10519  seq3coll  10525  crim  10570  fsumshftm  11154  isumshft  11199  cvgratgt0  11242  mertenslemi1  11244  negdvdsb  11405  dvdsnegb  11406  dvdsmul1  11411  dvdsabseq  11441  dvdsssfz1  11446  odd2np1  11466  ndvdsadd  11524  dvdssqim  11608  nn0seqcvgd  11618  algcvgblem  11626  cncongr2  11681  prmind2  11697  prmdvdsfz  11715  prmndvdsfaclt  11730  resttopon  12235  cnovex  12260  iscn  12261  iscnp  12263  cnco  12285  cndis  12305  hmeoco  12380  bl2in  12467  metss2lem  12561  metss2  12562  bdxmet  12565  metrest  12570  ioo2bl  12607  elcncf  12624  dvexp  12718  supfz  13039
  Copyright terms: Public domain W3C validator