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

Theorem syl2anr 278
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 277 . 2 ((𝜑𝜏) → 𝜃)
54ancoms 259 1 ((𝜏𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  swopo  4070  opswapg  4834  coexg  4889  iotass  4911  resdif  5175  fvexg  5221  isotr  5483  xpexgALT  5787  cauappcvgprlemladdfl  6810  addgt0sr  6917  axmulass  7004  axdistr  7005  negeu  7264  ltaddnegr  7493  nnsub  8027  zltnle  8347  elz2  8369  uzaddcl  8624  qaddcl  8666  xltneg  8849  xleneg  8850  iccneg  8957  uzsubsubfz  9012  fzsplit2  9015  fzss1  9027  uzsplit  9055  fz0fzdiffz0  9088  difelfzle  9093  difelfznle  9094  fzonlt0  9124  fzouzsplit  9136  eluzgtdifelfzo  9154  elfzodifsumelfzo  9158  ssfzo12  9181  qltnle  9202  modfzo0difsn  9339  nn0ennn  9367  isermono  9395  faclbnd  9602  bcval4  9613  bcpasc  9627  crim  9679  negdvdsb  10116  dvdsnegb  10117  dvdsmul1  10121  dvdsabseq  10151  dvdsssfz1  10156  odd2np1  10176  nn0seqcvgd  10235  algcvgblem  10243
  Copyright terms: Public domain W3C validator