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  6358  finnum  6363  ltsopi  6418  pitric  6419  pitri3or  6420  ltdcpi  6421  mulclpi  6426  addcompig  6427  mulcompig  6429  distrpig  6431  ltexpi  6435  ltapig  6436  ltmpig  6437  dfplpq2  6452  dfmpq2  6453  enqbreq2  6455  enqdc  6459  addcmpblnq  6465  addpipqqslem  6467  mulpipq2  6469  mulpipq  6470  mulpipqqs  6471  addclnq  6473  distrnqg  6485  ltdcnq  6495  ltrnqg  6518  enq0breq  6534  addclnq0  6549  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  distrnq0  6557  mulcomnq0  6558  genipv  6607  genplt2i  6608  genpelvl  6610  genpelvu  6611  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  addnqpr  6659  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  mulnqpr  6675  distrlem4prl  6682  distrlem4pru  6683  ltnqpr  6691  recexprlemloc  6729  archrecnq  6761  mulclsr  6839  1idsr  6853  00sr  6854  prsradd  6870  axmulass  6947  axdistr  6948  axcnre  6955  peano5nnnn  6966  mulid1  7024  axltadd  7089  lenlt  7094  cnegexlem3  7188  cnegex  7189  resubcl  7275  subeqrev  7374  muladd  7381  mulsub  7398  mulsub2  7399  ltaddsub2  7432  leaddsub2  7434  leltadd  7442  ltaddpos2  7448  posdif  7450  addge02  7468  mullt0  7475  recexre  7569  recextlem1  7632  recexap  7634  divmuldivap  7688  conjmulap  7705  prodgt02  7819  prodge02  7821  lemul2  7823  lemul2a  7825  ltmulgt12  7831  lemulge12  7833  ltmuldiv2  7841  ltdivmul2  7844  ledivmul2  7846  lemuldiv2  7848  cju  7913  peano5nni  7917  nnaddcl  7934  nnmulcl  7935  nnsub  7952  addltmul  8161  avgle1  8165  avgle2  8166  nnrecl  8179  nn0nnaddcl  8213  zsubcl  8286  zleloe  8292  znnsub  8296  zmulcl  8297  zltp1le  8298  zleltp1  8299  nnleltp1  8303  nnltp1le  8304  nnaddm1cl  8305  nn0ltp1le  8306  nn0leltp1  8307  nn0ltlem1  8308  znn0sub  8309  nn0sub  8310  elz2  8312  zapne  8315  zdcle  8317  zdclt  8318  zltlen  8319  nn0lem1lt  8323  nnlem1lt  8324  nnltlem1  8325  zdiv  8328  zextle  8331  zextlt  8332  btwnnz  8334  prime  8337  nneo  8341  peano2uz2  8345  peano5uzti  8346  uzind  8349  fzind  8353  fnn0ind  8354  uzneg  8491  uz11  8495  eluzp1m1  8496  eluzp1p1  8498  uzin  8505  indstr  8536  uz2mulcl  8545  qre  8560  qaddcl  8570  qsubcl  8573  qltlen  8575  irradd  8580  cnref1o  8582  rpaddcl  8606  rpmulcl  8607  rpdivcl  8608  elicc2  8807  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  fzval2  8877  elfz1eq  8899  peano2fzr  8901  fznlem  8905  fzsplit2  8914  fzaddel  8922  fzsubel  8923  fzrev2  8947  fzrev3  8949  uzsplit  8954  fzrevral  8967  fzrevral3  8969  fzshftral  8970  elfz2nn0  8973  elfz0addOLD  8980  fznn0sub2  8985  fz0fzdiffz0  8987  elfzmlbp  8990  difelfzle  8992  difelfznle  8993  1fv  8996  elfzouz2  9017  fzouzsplit  9035  elfzo0le  9041  fzonmapblen  9043  fzofzim  9044  fzoaddel2  9049  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  ubmelm1fzo  9082  fzofzp1b  9084  fzosplitprm1  9090  fzostep1  9093  subfzo0  9097  flqbi2  9133  divfl0  9138  flqzadd  9140  flqmulnn0  9141  frec2uzltd  9189  frec2uzrand  9191  frecfzen2  9204  iseqshft2  9232  iseqsplit  9238  iseqcaopr2  9241  expcllem  9266  expcl2lemap  9267  1exp  9284  expge1  9292  expadd  9297  expmul  9300  expsubap  9302  leexp1a  9309  lt2sq  9327  le2sq  9328  sumsqeq0  9332  bernneq  9369  bernneq2  9370  sq11ap  9414  shftfvalg  9419  shftf  9431  crre  9457  crim  9458  mulreap  9464  readd  9469  resub  9470  remul2  9473  imadd  9477  imsub  9478  immul2  9480  ipcnval  9486  cjsub  9492  cjreim  9503  caucvgre  9580  rexanuz  9587  rexuz3  9588  resqrexlemover  9608  resqrexlemcvg  9617  resqrexlemglsq  9620  sqrtle  9634  sqrtlt  9635  sqrt11ap  9636  sqrt11  9637  absreimsq  9665  absreim  9666  absmul  9667  sqabs  9678  absdiflt  9688  absdifle  9689  abssuble0  9699  abs2difabs  9704  fzomaxdif  9709  caubnd2  9713  climconst2  9812  climuni  9814  2clim  9822  climshft  9825  climshft2  9827  cjcn2  9836  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  climlec2  9861  sqrt2irr  9878  nn0seqcvgd  9880  ialgrlemconst  9882  ialgrp1  9885  ialgcvg  9887  ialgcvga  9890  bj-inex  10027  bj-bdfindis  10072
  Copyright terms: Public domain W3C validator