ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anr Structured version   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  addgt0sr  6663  axmulass  6717  axdistr  6718  negeu  6959  nnsub  7693  zltnle  8027  elz2  8048  uzaddcl  8265  qaddcl  8306  xltneg  8479  xleneg  8480  iccneg  8587  uzsubsubfz  8641  fzsplit2  8644  fzss1  8656  uzsplit  8684  fz0fzdiffz0  8717  difelfzle  8722  difelfznle  8723  fzonlt0  8753  fzouzsplit  8765  eluzgtdifelfzo  8783  elfzodifsumelfzo  8787  ssfzo12  8810  nn0ennn  8850  crim  9046
  Copyright terms: Public domain W3C validator