ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2an 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  2055  sylan9eq  2092  csbcomg  2873  sylan9ss  2958  ssconb  3076  ineqan12d  3140  dfopg  3547  breqan12d  3779  prelpwi  3950  opexg  3964  copsex2g  3983  ordin  4122  onin  4123  unexg  4178  eusv1  4184  op1stbg  4210  opelvvg  4389  opthprc  4391  opbrop  4419  relop  4486  dmpropg  4793  unixpm  4853  funssres  4942  funtp  4952  fnco  5007  resasplitss  5069  fodmrnu  5114  relrnfvex  5193  fconst2g  5376  fliftel  5433  oveqan12d  5531  ovi3  5637  ovg  5639  f1opw2  5706  off  5724  offres  5762  iunon  5899  nnsucsssuc  6071  nnaword1  6086  ertr  6121  erex  6130  brecop  6196  ecovdi  6217  ecovidi  6218  en2sn  6290  phplem4  6318  ssfiexmid  6336  diffitest  6344  ordiso  6356  finnum  6361  ltsopi  6416  pitric  6417  pitri3or  6418  ltdcpi  6419  mulclpi  6424  addcompig  6425  mulcompig  6427  distrpig  6429  ltexpi  6433  ltapig  6434  ltmpig  6435  dfplpq2  6450  dfmpq2  6451  enqbreq2  6453  enqdc  6457  addcmpblnq  6463  addpipqqslem  6465  mulpipq2  6467  mulpipq  6468  mulpipqqs  6469  addclnq  6471  distrnqg  6483  ltdcnq  6493  ltrnqg  6516  enq0breq  6532  addclnq0  6547  nqnq0a  6550  nqnq0m  6551  nq0m0r  6552  distrnq0  6555  mulcomnq0  6556  genipv  6605  genplt2i  6606  genpelvl  6608  genpelvu  6609  addnqprlemrl  6653  addnqprlemru  6654  addnqprlemfl  6655  addnqprlemfu  6656  addnqpr  6657  mulnqprlemrl  6669  mulnqprlemru  6670  mulnqprlemfl  6671  mulnqprlemfu  6672  mulnqpr  6673  distrlem4prl  6680  distrlem4pru  6681  ltnqpr  6689  recexprlemloc  6727  archrecnq  6759  mulclsr  6837  1idsr  6851  00sr  6852  prsradd  6868  axmulass  6945  axdistr  6946  axcnre  6953  peano5nnnn  6964  mulid1  7022  axltadd  7087  lenlt  7092  cnegexlem3  7186  cnegex  7187  resubcl  7273  subeqrev  7372  muladd  7379  mulsub  7396  mulsub2  7397  ltaddsub2  7430  leaddsub2  7432  leltadd  7440  ltaddpos2  7446  posdif  7448  addge02  7466  mullt0  7473  recexre  7567  recextlem1  7630  recexap  7632  divmuldivap  7686  conjmulap  7703  prodgt02  7817  prodge02  7819  lemul2  7821  lemul2a  7823  ltmulgt12  7829  lemulge12  7831  ltmuldiv2  7839  ltdivmul2  7842  ledivmul2  7844  lemuldiv2  7846  cju  7911  peano5nni  7915  nnaddcl  7932  nnmulcl  7933  nnsub  7950  addltmul  8159  avgle1  8163  avgle2  8164  nnrecl  8177  nn0nnaddcl  8211  zsubcl  8284  zleloe  8290  znnsub  8294  zmulcl  8295  zltp1le  8296  zleltp1  8297  nnleltp1  8301  nnltp1le  8302  nnaddm1cl  8303  nn0ltp1le  8304  nn0leltp1  8305  nn0ltlem1  8306  znn0sub  8307  nn0sub  8308  elz2  8310  zapne  8313  zdcle  8315  zdclt  8316  zltlen  8317  nn0lem1lt  8321  nnlem1lt  8322  nnltlem1  8323  zdiv  8326  zextle  8329  zextlt  8330  btwnnz  8332  prime  8335  nneo  8339  peano2uz2  8343  peano5uzti  8344  uzind  8347  fzind  8351  fnn0ind  8352  uzneg  8489  uz11  8493  eluzp1m1  8494  eluzp1p1  8496  uzin  8503  indstr  8534  uz2mulcl  8543  qre  8558  qaddcl  8568  qsubcl  8571  qltlen  8573  irradd  8578  cnref1o  8580  rpaddcl  8604  rpmulcl  8605  rpdivcl  8606  elicc2  8805  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  fzval2  8875  elfz1eq  8897  peano2fzr  8899  fznlem  8903  fzsplit2  8912  fzaddel  8920  fzsubel  8921  fzrev2  8945  fzrev3  8947  uzsplit  8952  fzrevral  8965  fzrevral3  8967  fzshftral  8968  elfz2nn0  8971  elfz0addOLD  8978  fznn0sub2  8983  fz0fzdiffz0  8985  elfzmlbp  8988  difelfzle  8990  difelfznle  8991  1fv  8994  elfzouz2  9015  fzouzsplit  9033  elfzo0le  9039  fzonmapblen  9041  fzofzim  9042  fzoaddel2  9047  eluzgtdifelfzo  9051  elfzodifsumelfzo  9055  ubmelm1fzo  9080  fzofzp1b  9082  fzosplitprm1  9088  fzostep1  9091  subfzo0  9095  flqbi2  9131  divfl0  9136  flqzadd  9138  flqmulnn0  9139  frec2uzltd  9163  frec2uzrand  9165  frecfzen2  9178  iseqshft2  9206  iseqsplit  9212  iseqcaopr2  9215  expcllem  9240  expcl2lemap  9241  1exp  9258  expge1  9266  expadd  9271  expmul  9274  expsubap  9276  leexp1a  9283  lt2sq  9301  le2sq  9302  sumsqeq0  9306  bernneq  9343  bernneq2  9344  sq11ap  9388  shftfvalg  9393  shftf  9405  crre  9431  crim  9432  mulreap  9438  readd  9443  resub  9444  remul2  9447  imadd  9451  imsub  9452  immul2  9454  ipcnval  9460  cjsub  9466  cjreim  9477  caucvgre  9554  rexanuz  9561  rexuz3  9562  resqrexlemover  9582  resqrexlemcvg  9591  resqrexlemglsq  9594  sqrtle  9608  sqrtlt  9609  sqrt11ap  9610  sqrt11  9611  absreimsq  9639  absreim  9640  absmul  9641  sqabs  9652  absdiflt  9662  absdifle  9663  abssuble0  9673  abs2difabs  9678  fzomaxdif  9683  caubnd2  9687  climconst2  9785  climuni  9787  2clim  9795  climshft  9798  climshft2  9800  cjcn2  9809  climaddc1  9822  climmulc2  9824  climsubc1  9825  climsubc2  9826  climlec2  9834  sqrt2irr  9851  nn0seqcvgd  9853  ialgrlemconst  9855  ialgrp1  9858  ialgcvg  9860  ialgcvga  9863  bj-inex  10000  bj-bdfindis  10045
  Copyright terms: Public domain W3C validator