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  6419  addclnq0  6434  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  distrnq0  6442  mulcomnq0  6443  genipv  6492  genplt2i  6493  genpelvl  6495  genpelvu  6496  addnqprlemrl  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  addnqpr  6542  distrlem4prl  6560  distrlem4pru  6561  recexprlemloc  6603  archrecnq  6635  mulclsr  6682  1idsr  6696  00sr  6697  axmulass  6757  axdistr  6758  axcnre  6765  mulid1  6822  axltadd  6886  lenlt  6891  cnegexlem3  6985  cnegex  6986  resubcl  7071  subeqrev  7170  muladd  7177  mulsub  7194  mulsub2  7195  ltaddsub2  7227  leaddsub2  7229  leltadd  7237  ltaddpos2  7243  posdif  7245  addge02  7263  mullt0  7270  recexre  7362  recextlem1  7414  recexap  7416  divmuldivap  7470  conjmulap  7487  prodgt02  7600  prodge02  7602  lemul2  7604  lemul2a  7606  ltmulgt12  7612  lemulge12  7614  ltmuldiv2  7622  ltdivmul2  7625  ledivmul2  7627  lemuldiv2  7629  cju  7694  peano5nni  7698  nnaddcl  7715  nnmulcl  7716  nnsub  7733  addltmul  7938  avgle1  7942  avgle2  7943  nnrecl  7955  nn0nnaddcl  7989  zsubcl  8062  zleloe  8068  znnsub  8072  zmulcl  8073  zltp1le  8074  zleltp1  8075  nnleltp1  8079  nnltp1le  8080  nnaddm1cl  8081  nn0ltp1le  8082  nn0leltp1  8083  nn0ltlem1  8084  znn0sub  8085  nn0sub  8086  elz2  8088  zapne  8091  zdcle  8093  zdclt  8094  zltlen  8095  nn0lem1lt  8099  nnlem1lt  8100  nnltlem1  8101  zdiv  8104  zextle  8107  zextlt  8108  btwnnz  8110  prime  8113  nneo  8117  peano2uz2  8121  peano5uzti  8122  uzind  8125  fzind  8129  fnn0ind  8130  uzneg  8267  uz11  8271  eluzp1m1  8272  eluzp1p1  8274  uzin  8281  indstr  8312  uz2mulcl  8321  qre  8336  qaddcl  8346  qsubcl  8349  irradd  8355  cnref1o  8357  rpaddcl  8381  rpmulcl  8382  rpdivcl  8383  elicc2  8577  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  fzval2  8647  elfz1eq  8669  peano2fzr  8671  fznlem  8675  fzsplit2  8684  fzaddel  8692  fzsubel  8693  fzrev2  8717  fzrev3  8719  uzsplit  8724  fzrevral  8737  fzrevral3  8739  fzshftral  8740  elfz2nn0  8743  elfz0addOLD  8750  fznn0sub2  8755  fz0fzdiffz0  8757  elfzmlbp  8760  difelfzle  8762  difelfznle  8763  1fv  8766  elfzouz2  8787  fzouzsplit  8805  elfzo0le  8811  fzonmapblen  8813  fzofzim  8814  fzoaddel2  8819  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  ubmelm1fzo  8852  fzofzp1b  8854  fzosplitprm1  8860  fzostep1  8863  frec2uzltd  8870  frec2uzrand  8872  frecfzen2  8885  expcllem  8920  expcl2lemap  8921  1exp  8938  expge1  8946  expadd  8951  expmul  8954  expsubap  8956  leexp1a  8963  lt2sq  8980  le2sq  8981  sumsqeq0  8985  bernneq  9022  bernneq2  9023  crre  9085  crim  9086  mulreap  9092  readd  9097  resub  9098  remul2  9101  imadd  9105  imsub  9106  immul2  9108  ipcnval  9114  cjsub  9120  cjreim  9131  bj-inex  9362  bj-bdfindis  9407
  Copyright terms: Public domain W3C validator