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

Theorem syl2an 273
Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
Hypotheses
Ref Expression
syl2an.1 (φψ)
syl2an.2 (τχ)
syl2an.3 ((ψ χ) → θ)
Assertion
Ref Expression
syl2an ((φ τ) → θ)

Proof of Theorem syl2an
StepHypRef Expression
1 syl2an.2 . 2 (τχ)
2 syl2an.1 . . 3 (φψ)
3 syl2an.3 . . 3 ((ψ χ) → θ)
42, 3sylan 267 . 2 ((φ χ) → θ)
51, 4sylan2 270 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:  syl2anr  274  anim12i  321  eqeqan12d  2037  sylan9eq  2074  csbcomg  2850  sylan9ss  2935  ssconb  3053  ineqan12d  3117  dfopg  3521  breqan12d  3753  prelpwi  3924  opexg  3938  copsex2g  3957  ordin  4071  onin  4072  unexg  4128  eusv1  4134  op1stbg  4160  opelvvg  4316  opthprc  4318  opbrop  4346  relop  4413  dmpropg  4720  unixpm  4780  funssres  4868  funtp  4878  fnco  4933  resasplitss  4994  fodmrnu  5039  relrnfvex  5118  fconst2g  5301  fliftel  5358  oveqan12d  5455  ovi3  5560  ovg  5562  f1opw2  5629  off  5647  offres  5685  iunon  5821  nnsucsssuc  5986  nnaword1  5997  ertr  6032  erex  6041  brecop  6107  ecovdi  6128  ecovidi  6129  ltsopi  6180  pitric  6181  pitri3or  6182  ltdcpi  6183  mulclpi  6188  addcompig  6189  mulcompig  6191  distrpig  6193  ltexpi  6197  ltapig  6198  ltmpig  6199  dfplpq2  6213  dfmpq2  6214  enqbreq2  6216  enqdc  6220  addcmpblnq  6226  addpipqqslem  6228  mulpipq2  6230  mulpipq  6231  mulpipqqs  6232  addclnq  6234  distrnqg  6246  ltdcnq  6256  ltrnqg  6277  enq0breq  6291  addclnq0  6306  nqnq0a  6309  nqnq0m  6310  nq0m0r  6311  distrnq0  6314  mulcomnq0  6315  genipv  6363  genplt2i  6364  genpelvl  6366  genpelvu  6367  distrlem4prl  6423  distrlem4pru  6424  recexprlemloc  6465  mulclsr  6501  1idsr  6515  00sr  6516  axmulass  6567  axdistr  6568  axcnre  6575  mulid1  6626  axltadd  6690  lenlt  6694  cnegexlem3  6775  cnegex  6776  resubcl  6861  subeqrev  6960  muladd  6967  mulsub  6984  mulsub2  6985  bj-inex  7130  bj-bdfindis  7169
  Copyright terms: Public domain W3C validator