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  2052  sylan9eq  2089  csbcomg  2867  sylan9ss  2952  ssconb  3070  ineqan12d  3134  dfopg  3538  breqan12d  3770  prelpwi  3941  opexg  3955  copsex2g  3974  ordin  4088  onin  4089  unexg  4144  eusv1  4150  op1stbg  4176  opelvvg  4332  opthprc  4334  opbrop  4362  relop  4429  dmpropg  4736  unixpm  4796  funssres  4885  funtp  4895  fnco  4950  resasplitss  5012  fodmrnu  5057  relrnfvex  5136  fconst2g  5319  fliftel  5376  oveqan12d  5474  ovi3  5579  ovg  5581  f1opw2  5648  off  5666  offres  5704  iunon  5840  nnsucsssuc  6010  nnaword1  6022  ertr  6057  erex  6066  brecop  6132  ecovdi  6153  ecovidi  6154  en2sn  6226  ssfiexmid  6254  ltsopi  6304  pitric  6305  pitri3or  6306  ltdcpi  6307  mulclpi  6312  addcompig  6313  mulcompig  6315  distrpig  6317  ltexpi  6321  ltapig  6322  ltmpig  6323  dfplpq2  6338  dfmpq2  6339  enqbreq2  6341  enqdc  6345  addcmpblnq  6351  addpipqqslem  6353  mulpipq2  6355  mulpipq  6356  mulpipqqs  6357  addclnq  6359  distrnqg  6371  ltdcnq  6381  ltrnqg  6403  enq0breq  6418  addclnq0  6433  nqnq0a  6436  nqnq0m  6437  nq0m0r  6438  distrnq0  6441  mulcomnq0  6442  genipv  6491  genplt2i  6492  genpelvl  6494  genpelvu  6495  addnqprlemrl  6537  addnqprlemru  6538  addnqprlemfl  6539  addnqprlemfu  6540  addnqpr  6541  distrlem4prl  6559  distrlem4pru  6560  recexprlemloc  6602  mulclsr  6662  1idsr  6676  00sr  6677  axmulass  6737  axdistr  6738  axcnre  6745  mulid1  6802  axltadd  6866  lenlt  6871  cnegexlem3  6965  cnegex  6966  resubcl  7051  subeqrev  7150  muladd  7157  mulsub  7174  mulsub2  7175  ltaddsub2  7207  leaddsub2  7209  leltadd  7217  ltaddpos2  7223  posdif  7225  addge02  7243  mullt0  7250  recexre  7342  recextlem1  7394  recexap  7396  divmuldivap  7450  conjmulap  7467  prodgt02  7580  prodge02  7582  lemul2  7584  lemul2a  7586  ltmulgt12  7592  lemulge12  7594  ltmuldiv2  7602  ltdivmul2  7605  ledivmul2  7607  lemuldiv2  7609  cju  7674  peano5nni  7678  nnaddcl  7695  nnmulcl  7696  nnsub  7713  addltmul  7918  avgle1  7922  avgle2  7923  nnrecl  7935  nn0nnaddcl  7969  zsubcl  8042  zleloe  8048  znnsub  8052  zmulcl  8053  zltp1le  8054  zleltp1  8055  nnleltp1  8059  nnltp1le  8060  nnaddm1cl  8061  nn0ltp1le  8062  nn0leltp1  8063  nn0ltlem1  8064  znn0sub  8065  nn0sub  8066  elz2  8068  zapne  8071  zdcle  8073  zdclt  8074  zltlen  8075  nn0lem1lt  8079  nnlem1lt  8080  nnltlem1  8081  zdiv  8084  zextle  8087  zextlt  8088  btwnnz  8090  prime  8093  nneo  8097  peano2uz2  8101  peano5uzti  8102  uzind  8105  fzind  8109  fnn0ind  8110  uzneg  8247  uz11  8251  eluzp1m1  8252  eluzp1p1  8254  uzin  8261  indstr  8292  uz2mulcl  8301  qre  8316  qaddcl  8326  qsubcl  8329  irradd  8335  cnref1o  8337  rpaddcl  8361  rpmulcl  8362  rpdivcl  8363  elicc2  8557  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  fzval2  8627  elfz1eq  8649  peano2fzr  8651  fznlem  8655  fzsplit2  8664  fzaddel  8672  fzsubel  8673  fzrev2  8697  fzrev3  8699  uzsplit  8704  fzrevral  8717  fzrevral3  8719  fzshftral  8720  elfz2nn0  8723  elfz0addOLD  8730  fznn0sub2  8735  fz0fzdiffz0  8737  elfzmlbp  8740  difelfzle  8742  difelfznle  8743  1fv  8746  elfzouz2  8767  fzouzsplit  8785  elfzo0le  8791  fzonmapblen  8793  fzofzim  8794  fzoaddel2  8799  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  ubmelm1fzo  8832  fzofzp1b  8834  fzosplitprm1  8840  fzostep1  8843  frec2uzltd  8850  frec2uzrand  8852  frecfzen2  8865  expcllem  8900  expcl2lemap  8901  1exp  8918  expge1  8926  expadd  8931  expmul  8934  expsubap  8936  leexp1a  8943  lt2sq  8960  le2sq  8961  sumsqeq0  8965  bernneq  9002  bernneq2  9003  crre  9065  crim  9066  mulreap  9072  readd  9077  resub  9078  remul2  9081  imadd  9085  imsub  9086  immul2  9088  ipcnval  9094  cjsub  9100  cjreim  9111  bj-inex  9338  bj-bdfindis  9381
  Copyright terms: Public domain W3C validator