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

Theorem syl2an 283
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 277 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2 280 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  syl2anr  284  anim12i  331  syl2an2  559  syl2an2r  560  mp3an3an  1277  eqeqan12d  2100  sylan9eq  2137  csbcomg  2943  sylan9ss  3027  ssconb  3122  ineqan12d  3192  dfopg  3605  breqan12d  3837  opexg  4031  copsex2g  4049  ordin  4188  onin  4189  unexg  4244  eusv1  4250  opelvvg  4457  opthprc  4459  opbrop  4487  relop  4556  dmpropg  4871  unixpm  4934  funssres  5023  funinsn  5030  funtp  5034  fnco  5089  resasplitss  5155  fodmrnu  5206  relrnfvex  5288  fconst2g  5475  oveqan12d  5634  ovi3  5740  ovg  5742  f1opw2  5809  off  5827  offres  5865  iunon  6005  nnsucsssuc  6209  nnaword1  6226  ertr  6261  erex  6270  brecop  6336  ecovdi  6357  ecovidi  6358  mapvalg  6369  pmvalg  6370  pmss12g  6386  mapsn  6401  en2sn  6484  xpf1o  6514  xpen  6515  phplem4  6525  ssfilem  6545  diffitest  6557  en1eqsn  6609  sbthlem7  6619  ordiso  6676  updjud  6720  fodjuomnilem0  6749  finnum  6758  pr2nelem  6766  ltsopi  6826  pitric  6827  pitri3or  6828  ltdcpi  6829  mulclpi  6834  addcompig  6835  mulcompig  6837  distrpig  6839  ltexpi  6843  ltapig  6844  ltmpig  6845  dfplpq2  6860  dfmpq2  6861  enqbreq2  6863  enqdc  6867  addcmpblnq  6873  addpipqqslem  6875  mulpipq2  6877  mulpipq  6878  mulpipqqs  6879  addclnq  6881  distrnqg  6893  ltdcnq  6903  ltrnqg  6926  enq0breq  6942  addclnq0  6957  nqnq0a  6960  nqnq0m  6961  nq0m0r  6962  distrnq0  6965  mulcomnq0  6966  genipv  7015  genplt2i  7016  genpelvl  7018  genpelvu  7019  addnqprlemrl  7063  addnqprlemru  7064  addnqprlemfl  7065  addnqprlemfu  7066  addnqpr  7067  mulnqprlemrl  7079  mulnqprlemru  7080  mulnqprlemfl  7081  mulnqprlemfu  7082  mulnqpr  7083  distrlem4prl  7090  distrlem4pru  7091  ltnqpr  7099  recexprlemloc  7137  archrecnq  7169  mulclsr  7247  1idsr  7261  00sr  7262  prsradd  7278  axmulass  7355  axdistr  7356  axcnre  7363  peano5nnnn  7374  mulid1  7432  axltadd  7503  lenlt  7508  cnegexlem3  7606  cnegex  7607  resubcl  7693  subeqrev  7801  muladd  7809  mulsub  7826  mulsub2  7827  ltaddsub2  7862  leaddsub2  7864  leltadd  7872  ltaddpos2  7878  posdif  7880  addge02  7898  mullt0  7905  recexre  7999  recextlem1  8062  recexap  8064  divmuldivap  8121  conjmulap  8138  prodgt02  8252  prodge02  8254  lemul2  8256  lemul2a  8258  ltmulgt12  8264  lemulge12  8266  ltmuldiv2  8274  ltdivmul2  8277  ledivmul2  8279  lemuldiv2  8281  negiso  8354  cju  8359  peano5nni  8363  nnaddcl  8380  nnmulcl  8381  nnsub  8398  addltmul  8588  avgle1  8592  avgle2  8593  nnrecl  8607  nn0nnaddcl  8640  zsubcl  8727  zleloe  8733  znnsub  8737  nzadd  8738  zmulcl  8739  zltp1le  8740  zleltp1  8741  nnleltp1  8745  nnltp1le  8746  nnaddm1cl  8747  nn0ltp1le  8748  nn0leltp1  8749  nn0ltlem1  8750  znn0sub  8751  nn0sub  8752  elz2  8754  zapne  8757  zdcle  8759  zdclt  8760  zltlen  8761  nn0lem1lt  8765  nnlem1lt  8766  nnltlem1  8767  zdiv  8770  zextle  8773  zextlt  8774  btwnnz  8776  prime  8781  nneo  8785  peano2uz2  8789  peano5uzti  8790  uzind  8793  fzind  8797  fnn0ind  8798  uzneg  8972  uz11  8976  eluzp1m1  8977  eluzp1p1  8979  uzin  8986  indstr  9016  uz2mulcl  9030  qre  9045  qaddcl  9055  qsubcl  9058  qltlen  9060  qlttri2  9061  irradd  9066  cnref1o  9068  rpaddcl  9092  rpmulcl  9093  rpdivcl  9094  elicc2  9291  iccshftr  9346  iccshftl  9348  iccdil  9350  icccntr  9352  fzval2  9362  elfz1eq  9384  peano2fzr  9386  fznlem  9390  fzsplit2  9399  fzaddel  9407  fzsubel  9408  fzrev2  9432  fzrev3  9434  uzsplit  9439  fzrevral  9452  fzrevral3  9454  fzshftral  9455  elfz2nn0  9459  fznn0sub2  9470  fz0fzdiffz0  9472  elfzmlbp  9474  difelfzle  9476  difelfznle  9477  1fv  9481  elfzouz2  9503  fzouzsplit  9521  elfzo0le  9527  fzonmapblen  9529  fzofzim  9530  fzoaddel2  9535  eluzgtdifelfzo  9539  elfzodifsumelfzo  9543  ubmelm1fzo  9568  fzofzp1b  9570  fzosplitprm1  9576  fzostep1  9579  subfzo0  9584  qbtwnxr  9600  flqbi2  9629  divfl0  9634  flqzadd  9636  flqmulnn0  9637  addmodidr  9711  modfzo0difsn  9733  frec2uzltd  9741  frec2uzrand  9743  frecfzen2  9765  iseqshft2  9810  iseqsplit  9816  iseqcaopr2  9819  expcllem  9868  expcl2lemap  9869  1exp  9886  expge1  9894  expadd  9899  expmul  9902  expsubap  9905  leexp1a  9912  lt2sq  9930  le2sq  9931  sumsqeq0  9935  bernneq  9974  bernneq2  9975  sq11ap  10020  facdiv  10046  faclbnd  10049  faclbnd3  10051  faclbnd6  10052  facavg  10054  bcrpcl  10061  bccmpl  10062  iseqcoll  10147  shftfvalg  10152  shftf  10164  crre  10190  crim  10191  mulreap  10197  readd  10202  resub  10203  remul2  10206  imadd  10210  imsub  10211  immul2  10213  ipcnval  10219  cjsub  10225  cjreim  10236  caucvgre  10313  rexanuz  10320  rexuz3  10322  resqrexlemover  10342  resqrexlemcvg  10351  resqrexlemglsq  10354  sqrtle  10368  sqrtlt  10369  sqrt11ap  10370  sqrt11  10371  absreimsq  10399  absreim  10400  absmul  10401  sqabs  10414  absdiflt  10424  absdifle  10425  abssuble0  10435  abs2difabs  10440  fzomaxdif  10445  caubnd2  10449  zmaxcl  10555  minmax  10559  min1inf  10560  min2inf  10561  climconst2  10577  climuni  10579  2clim  10587  climshft  10590  climshft2  10592  cjcn2  10601  climaddc1  10614  climmulc2  10616  climsubc1  10617  climsubc2  10618  climlec2  10626  isummolem2a  10665  zisum  10668  dvdssub2  10744  dvdsadd  10745  dvdsaddr  10746  dvdssub  10747  dvdssubr  10748  fzocongeq  10765  odd2np1  10779  opoe  10801  omoe  10802  opeo  10803  omeo  10804  divalgb  10831  ndvdsadd  10837  zsupcllemstep  10847  gcdabs  10885  dvdsgcd  10907  absmulgcd  10912  gcdmultiple  10915  gcdmultiplez  10916  rpmulgcd  10921  sqgcd  10924  dvdssqlem  10925  dvdssq  10926  nn0seqcvgd  10929  ialgrlemconst  10931  ialgrp1  10934  ialgcvg  10936  ialgcvga  10939  lcmval  10951  lcmabs  10964  lcmgcd  10966  lcmdvds  10967  lcmgcdnn  10970  coprmgcdb  10976  coprmdvds  10980  coprmdvds2  10981  qredeq  10984  isprm3  11006  nprm  11011  divgcdodd  11028  prmdvdsexp  11033  sqrt2irr  11047  zgcdsq  11085  hashdvds  11103  phiprmpw  11104  crth  11106  phimullem  11107  bj-inex  11267  bj-bdfindis  11311
  Copyright terms: Public domain W3C validator