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

Theorem syl2an 287
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 281 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2 284 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  syl2anr  288  anim12i  336  syl2an2  568  syl2an2r  569  mp3an3an  1306  eqeqan12d  2133  sylan9eq  2170  csbcomg  2996  sylan9ss  3080  ssconb  3179  ineqan12d  3249  dfopg  3673  breqan12d  3915  opexg  4120  copsex2g  4138  ordin  4277  onin  4278  unexg  4334  eusv1  4343  opelvvg  4558  opthprc  4560  opbrop  4588  relop  4659  dmpropg  4981  unixpm  5044  funssres  5135  funinsn  5142  funtp  5146  fnco  5201  resasplitss  5272  fodmrnu  5323  relrnfvex  5407  fconst2g  5603  oveqan12d  5761  ovi3  5875  ovg  5877  f1opw2  5944  off  5962  offres  6001  iunon  6149  nnsucsssuc  6356  nnaword1  6377  ertr  6412  erex  6421  brecop  6487  ecovdi  6508  ecovidi  6509  mapvalg  6520  pmvalg  6521  pmss12g  6537  mapsn  6552  en2sn  6675  xpf1o  6706  xpen  6707  phplem4  6717  ssfilem  6737  diffitest  6749  en1eqsn  6804  sbthlem7  6819  ordiso  6889  updjud  6935  fodju0  6987  finnum  7007  pr2nelem  7015  djucomen  7040  ltsopi  7096  pitric  7097  pitri3or  7098  ltdcpi  7099  mulclpi  7104  addcompig  7105  mulcompig  7107  distrpig  7109  ltexpi  7113  ltapig  7114  ltmpig  7115  dfplpq2  7130  dfmpq2  7131  enqbreq2  7133  enqdc  7137  addcmpblnq  7143  addpipqqslem  7145  mulpipq2  7147  mulpipq  7148  mulpipqqs  7149  addclnq  7151  distrnqg  7163  ltdcnq  7173  ltrnqg  7196  enq0breq  7212  addclnq0  7227  nqnq0a  7230  nqnq0m  7231  nq0m0r  7232  distrnq0  7235  mulcomnq0  7236  genipv  7285  genplt2i  7286  genpelvl  7288  genpelvu  7289  addnqprlemrl  7333  addnqprlemru  7334  addnqprlemfl  7335  addnqprlemfu  7336  addnqpr  7337  mulnqprlemrl  7349  mulnqprlemru  7350  mulnqprlemfl  7351  mulnqprlemfu  7352  mulnqpr  7353  distrlem4prl  7360  distrlem4pru  7361  ltnqpr  7369  recexprlemloc  7407  archrecnq  7439  mulclsr  7530  1idsr  7544  00sr  7545  prsradd  7562  axmulass  7649  axdistr  7650  axcnre  7657  peano5nnnn  7668  mulid1  7731  axltadd  7802  lenlt  7808  cnegexlem3  7907  cnegex  7908  resubcl  7994  subeqrev  8106  muladd  8114  mulsub  8131  mulsub2  8132  ltaddsub2  8167  leaddsub2  8169  leltadd  8177  ltaddpos2  8183  posdif  8185  addge02  8203  mullt0  8210  recexre  8307  recextlem1  8379  recexap  8381  divmuldivap  8439  conjmulap  8456  div2subap  8563  prodgt02  8575  prodge02  8577  lemul2  8579  lemul2a  8581  ltmulgt12  8587  lemulge12  8589  ltmuldiv2  8597  ltdivmul2  8600  ledivmul2  8602  lemuldiv2  8604  negiso  8677  cju  8683  peano5nni  8687  nnaddcl  8704  nnmulcl  8705  nnsub  8723  addltmul  8914  avgle1  8918  avgle2  8919  nnrecl  8933  nn0nnaddcl  8966  zsubcl  9053  zleloe  9059  znnsub  9063  nzadd  9064  zmulcl  9065  zltp1le  9066  zleltp1  9067  nnleltp1  9071  nnltp1le  9072  nnaddm1cl  9073  nn0ltp1le  9074  nn0leltp1  9075  nn0ltlem1  9076  znn0sub  9077  nn0sub  9078  elz2  9080  zapne  9083  zdcle  9085  zdclt  9086  zltlen  9087  nn0lem1lt  9092  nnlem1lt  9093  nnltlem1  9094  zdiv  9097  zextle  9100  zextlt  9101  btwnnz  9103  prime  9108  nneo  9112  peano2uz2  9116  peano5uzti  9117  uzind  9120  fzind  9124  fnn0ind  9125  uzneg  9300  uz11  9304  eluzp1m1  9305  eluzp1p1  9307  uzin  9314  indstr  9344  uz2mulcl  9358  qre  9373  qaddcl  9383  qsubcl  9386  qltlen  9388  qlttri2  9389  irradd  9394  cnref1o  9396  rpaddcl  9420  rpmulcl  9421  rpdivcl  9422  rexadd  9590  rexsub  9591  xaddcom  9599  xnn0xadd0  9605  xnegdi  9606  elicc2  9676  iccshftr  9732  iccshftl  9734  iccdil  9736  icccntr  9738  fzval2  9748  elfz1eq  9770  peano2fzr  9772  fznlem  9776  fzsplit2  9785  fzaddel  9794  fzsubel  9795  fzrev2  9820  fzrev3  9822  uzsplit  9827  fzrevral  9840  fzrevral3  9842  fzshftral  9843  elfz2nn0  9847  fznn0sub2  9860  fz0fzdiffz0  9862  elfzmlbp  9864  difelfzle  9866  difelfznle  9867  1fv  9871  elfzouz2  9893  fzouzsplit  9911  elfzo0le  9917  fzonmapblen  9919  fzofzim  9920  fzoaddel2  9925  eluzgtdifelfzo  9929  elfzodifsumelfzo  9933  ubmelm1fzo  9958  fzofzp1b  9960  fzosplitprm1  9966  fzostep1  9969  subfzo0  9974  qbtwnxr  9990  flqbi2  10019  divfl0  10024  flqzadd  10026  flqmulnn0  10027  addmodidr  10101  modfzo0difsn  10123  frec2uzltd  10131  frec2uzrand  10133  frecfzen2  10155  seq3split  10207  seq3caopr2  10210  exp3vallem  10249  expcllem  10259  expcl2lemap  10260  1exp  10277  expge1  10285  expadd  10290  expmul  10293  expsubap  10296  leexp1a  10303  lt2sq  10321  le2sq  10322  sumsqeq0  10326  bernneq  10367  bernneq2  10368  sq11ap  10413  facdiv  10439  faclbnd  10442  faclbnd3  10444  faclbnd6  10445  facavg  10447  bcrpcl  10454  bccmpl  10455  seq3coll  10540  shftfvalg  10545  shftf  10557  crre  10584  crim  10585  mulreap  10591  readd  10596  resub  10597  remul2  10600  imadd  10604  imsub  10605  immul2  10607  ipcnval  10613  cjsub  10619  cjreim  10630  caucvgre  10708  rexanuz  10715  rexuz3  10717  resqrexlemover  10737  resqrexlemcvg  10746  resqrexlemglsq  10749  sqrtle  10763  sqrtlt  10764  sqrt11ap  10765  sqrt11  10766  absreimsq  10794  absreim  10795  absmul  10796  sqabs  10809  absdiflt  10819  absdifle  10820  abssuble0  10830  abs2difabs  10835  fzomaxdif  10840  caubnd2  10844  rpmaxcl  10950  zmaxcl  10951  minmax  10956  mincl  10957  min1inf  10958  min2inf  10959  minabs  10962  minclpr  10963  rpmincl  10964  xrmaxrecl  10979  xrminmax  10989  xrmincl  10990  xrmin1inf  10991  xrmin2inf  10992  xrminrecl  10997  xrminrpcl  10998  iooinsup  11001  climconst2  11015  climuni  11017  2clim  11025  climshft  11028  climshft2  11030  cjcn2  11040  climaddc1  11053  climmulc2  11055  climsubc1  11056  climsubc2  11057  climlec2  11065  summodclem2a  11105  zsumdc  11108  isumclim3  11147  mptfzshft  11166  fsumrev  11167  fisum0diag2  11171  telfsumo2  11191  fsumparts  11194  cvgcmpub  11200  binomlem  11207  binom1p  11209  binom1dif  11211  bcxmas  11213  isumshft  11214  expcnvap0  11226  expcnv  11228  geosergap  11230  geolim  11235  cvgratnnlemrate  11254  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcj  11293  eftlub  11310  effsumlt  11312  efieq  11356  sinsub  11361  cossub  11362  subsin  11364  sinmul  11365  cosmul  11366  addcos  11367  subcos  11368  dvdssub2  11447  dvdsadd  11448  dvdsaddr  11449  dvdssub  11450  dvdssubr  11451  fzocongeq  11468  odd2np1  11482  opoe  11504  omoe  11505  opeo  11506  omeo  11507  divalgb  11534  ndvdsadd  11540  zsupcllemstep  11550  gcdabs  11588  dvdsgcd  11612  absmulgcd  11617  gcdmultiple  11620  gcdmultiplez  11621  rpmulgcd  11626  sqgcd  11629  dvdssqlem  11630  dvdssq  11631  nn0seqcvgd  11634  ialgrlemconst  11636  algrf  11638  algrp1  11639  algcvg  11641  algcvga  11644  lcmval  11656  lcmabs  11669  lcmgcd  11671  lcmdvds  11672  lcmgcdnn  11675  coprmgcdb  11681  coprmdvds  11685  coprmdvds2  11686  qredeq  11689  isprm3  11711  nprm  11716  divgcdodd  11733  prmdvdsexp  11738  sqrt2irr  11752  zgcdsq  11790  hashdvds  11808  phiprmpw  11809  crth  11811  phimullem  11812  setsvalg  11900  setsfun0  11906  restval  12037  innei  12243  cnovex  12276  txuni2  12336  txbasex  12337  txbas  12338  txtop  12340  txtopon  12342  txss12  12346  txbasval  12347  txcnp  12351  upxp  12352  txcnmpt  12353  uptx  12354  txcn  12355  txrest  12356  txdis  12357  cnmpt21  12371  hmeoco  12396  txhmeo  12399  isxmet2d  12428  blin2  12512  comet  12579  metcn  12594  txmetcn  12599  qtopbasss  12601  qtopbas  12602  remetdval  12619  bl2ioo  12622  blssioo  12625  divcnap  12635  cncfmet  12659  dvaddxxbr  12745  dvcjbr  12752  sinperlem  12800  sincosq2sgn  12819  sincosq3sgn  12820  bj-inex  13001  bj-bdfindis  13041  triap  13120  cvgcmp2nlemabs  13123  trilpolemisumle  13127  inffz  13134
  Copyright terms: Public domain W3C validator