ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anr GIF 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  6627  addgt0sr  6703  axmulass  6757  axdistr  6758  negeu  6999  nnsub  7733  zltnle  8067  elz2  8088  uzaddcl  8305  qaddcl  8346  xltneg  8519  xleneg  8520  iccneg  8627  uzsubsubfz  8681  fzsplit2  8684  fzss1  8696  uzsplit  8724  fz0fzdiffz0  8757  difelfzle  8762  difelfznle  8763  fzonlt0  8793  fzouzsplit  8805  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  ssfzo12  8850  nn0ennn  8890  crim  9086
  Copyright terms: Public domain W3C validator