Theorem sylib 215

Description: A mixed syllogism inference from an implication and a biconditional.

Hypotheses

Ref	Expression
sylib.1	|- (ph -> ps)
sylib.2	|- (ps <-> ch)

Assertion

Ref	Expression
sylib	|- (ph -> ch)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 |- (ph -> ps)
2		sylib.2	. . 3 |- (ps <-> ch)
3	2	biimpi 168	. 2 |- (ps -> ch)
4	1, 3	syl 12	1 |- (ph -> ch)

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  3imtr3i 235  ord 249  exp3a 405  ancomd 483  imdistand 493  bicomd 580  pm2.85 639  pm5.74d 645  mpbidi 649  notbid 673  pm4.71rd 701  pm5.32d 709  pm5.18OLD 723  ecase2d 824  consensusOLD 845  dn1 855  3mix3 1047  ecase23d 1198  nic-ax 1239  excomim 1392  19.23aiOLD 1413  19.23ad 1415  nexd 1457  sbf 1551  hbs1fOLD 1556  sbiedOLD 1564  sbequi 1598  sbn 1601  a4sbe 1613  a4sbimOLD 1615  a4sbbi 1616  sb6rf 1635  sb6rfOLD 1636  sb8OLD 1638  sb9i 1640  eu2 1791  mooran1OLD 1823  euor2OLD 1840  2euex 1844  2eu1 1853  eqcomd 1889  necon1bi 2048  necon2bi 2053  necon2i 2054  necon4ai 2067  necon4i 2069  necon4iOLD 2070  necomd 2095  r19.21bi 2188  nrexdv 2193  r19.23ad 2213  elex 2302  ceqsalgOLD 2315  cla4gf 2361  cla4gfOLD 2363  euind 2439  reuind 2450  3sstr3g 2657  syl6ss 2663  sseq0OLD 2904  un00 2907  npss0OLD 2912  disjpss 2924  ssnelpss 2937  pssnel 2938  tpid3g 3115  difsnid 3131  sneqr 3147  preqr1 3152  preq12b 3154  reucl 3213  uniintsn 3253  ssiunOLD 3294  iinrab2 3319  iununi 3331  iununiOLD 3332  3brtr3g 3368  trint 3426  axrep1 3429  axrep2 3430  axrep4 3432  axrep5 3433  class2set 3471  0inp0 3475  pwel 3506  exss 3516  opth1 3531  opthwiener 3554  pwssun 3578  sotric 3615  sotrieq 3616  efrn2lp 3638  wecmpep 3650  wereu 3654  ordtri3or 3691  ordtri3orOLD 3692  ordtri1 3693  ordtri1OLD 3694  ordtri3 3697  ordtri3OLD 3698  suctr 3751  ordnbtwn 3761  orddif 3764  orduniss 3765  ordtri2orOLD 3767  suc11 3773  onelini 3781  oneluni 3782  on0eqel 3787  difex2OLD 3803  euuni 3807  euexeqOLD 3826  euexaleq 3827  eufromeq2 3829  eufromeq6 3833  euobj1 3834  rabxfrd 3842  reuxfr2d 3844  reuxfr2 3845  reuhypd 3848  iunpw 3858  epne3 3860  dfwe2OLD 3862  ordeleqon 3866  sucexg 3891  suceloni 3894  ordunisuc 3911  ordunisucOLD 3912  onuninsuci 3921  ordunisuc2 3926  dflim3OLD 3931  limsssuc 3934  tfi 3937  tfindsg2 3945  findOLD 3978  finds2 3981  ssrel 4075  ssrelOLD 4076  ssrelrel 4083  ssrelrelOLD 4084  elrel 4086  xpsspw 4093  relop 4113  opelxpex2OLD 4120  dmxp 4177  dmxpOLD 4178  resopab2 4256  relimasn 4288  ndmima 4300  funeu 4444  funopg 4454  funun 4462  funtp 4468  funcnvuni 4482  funinOLD 4485  funcnvres2 4489  imadif 4493  fneu2 4519  fn0OLD 4533  fnopabg 4546  fcoi2OLD 4587  fcnvres 4589  f00 4601  foconst 4629  foimacnv 4657  resdif 4659  resin 4660  f1ococnv2 4662  f1ococnv1 4663  fvprc 4678  fv3 4690  tz6.12-2 4696  dffv2 4734  fvopabn 4749  elrnopabg 4773  exfo 4795  fopab2 4796  fsn 4807  fnressn 4812  funoprabg 4939  1stcof 5040  elrnoprabg 5066  curry1 5075  curry1f 5076  curry2 5078  curry2f 5079  onopriun 5118  tfrlem5 5123  tfrlem8 5126  tz7.48-2 5166  abianfp 5171  oalimcl 5242  omlimcl 5257  brecop2 5366  ecopoprdm 5368  mapsn 5404  ixp0 5420  en2d 5459  dom2d 5463  fundmen 5487  unen 5493  pw2en 5505  ac6sfilem3 5508  sbthlem3 5512  sbthlem4 5513  sbthlem5 5514  sbthlem6 5515  sdomdomtr 5532  fodomr 5547  xpen 5582  mapenlem2 5584  mapdom2 5588  xpmapenlem3 5592  xpmapenlem5 5594  mapunen 5596  pwen 5597  ssenen 5598  nneneq 5606  php 5607  isfinite1 5624  infn0 5626  ssfi 5630  unblem2 5634  isfinite2 5639  unfi 5644  unifi 5648  fiint 5650  abfii2 5652  pwfilem 5660  ordiso 5683  ordtypelem4 5687  ordtypelem6 5689  ordtypelem7 5690  hartog 5693  zfregcl 5697  elirrv 5700  inf3lem3 5721  inf3lem6 5724  infeq5 5727  noinfep 5747  zfregs 5754  zfregs2 5755  r1val1 5769  rankr1 5785  rankuni 5809  rankval4 5813  rankc2 5817  rankelun 5818  rankelpr 5819  rankelop 5820  rankxplim 5823  rankxplim3 5825  rankxpsuc 5826  ordelordaxr 5833  hta 5858  omsubsdomlem2 5880  infenomsub 5889  aceq3lem 5894  aceq5lem4 5900  aceq5 5902  ac6lem 5916  ac9s 5926  kmlem1 5927  kmlem4 5930  kmlem5 5931  kmlem7 5933  kmlem11 5937  zorn2lem4 5953  zorn2lem6 5955  zorn 5959  fodomb 5962  brdom3 5963  brdom5 5964  brdom4 5965  imadomg 5968  ficardom 5979  cardmin 6012  cardprc 6013  alephnbtwn 6016  cardaleph 6033  alephval3 6051  cflem 6053  cfval 6054  cfeq0 6062  cdaval 6067  nd1 6090  nd2 6091  axpownd 6105  zfcndext 6117  zfcndrep 6118  distrpq 6219  prn0 6245  prnmax 6251  genpn0 6258  genpnnp 6260  prlem934 6291  ltaddpr 6292  prlem936 6307  reclem2pr 6309  suplem1pr 6313  suppsr 6374  supsrlem6 6382  ltresr 6410  supre 6412  negeui 6510  lttri4OLD 6685  ltnsym2OLD 6704  renfdisjOLD 6713  xrltnsym2 6726  xrrebnd 6743  receui 6890  rec11ii 6953  eqnegi 6982  nnind 7120  nn1suc 7122  nnleltp1 7138  nominpos 7230  lble 7256  bndndx 7282  xrsupsslem 7285  xrinfmsslem 7286  xrsupss 7287  xrinfmss 7288  supxrre 7292  elnnz 7354  elnnz1 7364  uzwo3 7431  icounlem 7581  snunioolem 7583  uzwo 7624  uzwoOLD 7625  nnwof 7628  elfzp1 7683  fzprval 7687  fztpval 7688  fzneuz 7697  expnnval 7815  discrlem3 7908  nn0opthlem2 7915  nn0opthi 7916  sqrlem13 7935  sqr2irrlem3 7976  crulem 7986  crne0i 7989  creui 7993  replim 8011  abssubne0 8134  cvg1 8173  cvg2i 8174  cvg3i 8175  faclbnd4lem4 8203  dffsum 8258  serzfsum 8264  fsump1s 8273  fsum1ps 8278  fsumshft 8291  fsumcmp 8300  bcxmas 8336  clm3i 8339  climreu 8361  climrecl 8370  climge0 8372  climubii 8413  dfisum 8452  infcvglem1 8482  infcvglem3 8484  cvgratlem5 8516  fsum0diag4 8523  cncffvrn 8535  abscncflem 8536  mulc1cncf 8541  ivthlem3 8545  ivthlem5 8547  ivthlem6 8548  ivthlem7 8549  efseq0ex 8573  efcl 8574  efcvg 8576  efcvgfsum 8577  reeftlcl 8642  eflti 8671  efcnlem1 8684  efcn 8688  acdc5lem1 8760  acdcALT 8765  unbenlem 8773  infxpidmlem7 8827  infxpidmlem8 8828  infxpidmlem10 8830  infxpidmlem11 8831  infxpidmlem12 8832  infpss 8843  iunctb 8844  basgen2 8909  subbas 8914  fctop 8920  cctop 8922  clsval 8953  uncld 8957  ntrval2 8962  cmclsopn 8969  cmntrcld 8970  elcls 8980  neif 8991  0nnei 9002  islp2 9023  clslp 9024  qdensere 9027  idcn 9042  ismsg 9077  metreslem 9099  blf 9121  cncfmet 9183  lmuni 9229  lmsslem 9230  lmfexlem1 9234  metcnp4 9248  xplmi 9251  xpcn 9254  oprcn 9255  bopcnlem1 9259  bopcnlem4 9262  bcthlem4 9280  bcthlem7 9283  bcthlem9 9285  bcthlem14 9290  bcthlem28 9304  bcthlem29 9305  bcthlem30 9306  bcthlem31 9307  bcthlem33 9309  grpideu 9333  grprn 9336  isgrp2i 9360  grpinvf 9364  grpdivf 9370  gxpval 9382  gxnval 9383  resgrprn 9403  grplactf1o 9406  ssga 9455  gapm 9462  vcex 9531  nvvcop 9545  nvvop 9560  nvex 9562  nvmf 9598  vacnlem6 9672  sqcn 9674  va1cnlem 9684  ipf 9705  ip1cnilem2 9713  ip1cnilem3 9714  nmlno0lem 9793  siilem1 9852  ipblnfi 9857  ubthlem3 9874  minveclem26 9915  pilem1 10020  pilem2 10021  sinperlem2 10036  sincosq2sgn 10054  sincosq4sgn 10056  efifolem2 10077  efif1lem5 10088  efif1lem7 10090  grothomex 10136  oprabopabf 10157  dif1en 10172  indexfi 10174  basmetres 10185  upxp 10225  uptx 10226  txcnopab 10228  cnvhmpha 10240  subspid 10249  subtopmetlem 10255  fipfil2 10272  fbunfip 10282  fgfil 10290  extbas1 10291  extbas2 10292  filrn 10293  elfilmap 10312  cncomp 10331  dirtr 10356  axhcompl 10500  bcseqi 10619  chcmhi 10746  norm1exi 10755  shorth 10801  occllem4 10809  projlem24 10842  pjthlem11 10862  pjtheu2i 10883  pjoc1i 10897  spanval 10932  hsupval2 10933  shlej1i 10981  shs00i 11006  chj00i 11043  chabs2 11073  h1de2i 11109  cmbr4i 11177  spansnm0i 11230  nonbooli 11231  5oalem5 11238  pjssmii 11261  pjvec 11276  pjocvec 11277  hoaddcl 11321  homulcl 11322  eigposi 11399  dmadjop 11457  brafn 11508  kbop 11514  nmlnop0iALT 11557  lnopeq0i 11569  nmcopexlem4 11591  nmcfnexlem4 11620  cnlnadjlem2 11638  cnlnadjlem3 11639  cnlnadjlem4 11640  cnlnadjlem5 11641  cnlnssadj 11650  nmopcoi 11665  cnvbraval 11681  kbass2 11688  pjss1coi 11735  pjss2coi 11736  pjorthcoi 11741  pjscji 11742  pjssdif2i 11746  pjssdif1i 11747  pjclem4 11772  pjci 11773  pj3si 11780  pj3cor1i 11782  strlem3a 11824  strlem6 11828  hstrlem3a 11832  hstrlem6 11836  mdbr3 11869  mdbr4 11870  dmdbr5 11880  ssmd2 11884  mdslj1i 11891  mdslj2i 11892  mdsl2bi 11895  cvmdi 11896  mdslmd1lem1 11897  mdslmd1lem2 11898  hatomistici 11934  chrelat2i 11937  atssma 11950  atoml2i 11955  irredlem1 11962  irredlem2 11963  mdsymlem1 11975  mdsymlem2 11976  mdsymlem5 11979  dmdbr4ati 11993  dmdbr5ati 11994  bnj24 12388  bnj44OLD 12420  bnj48OLD 12423  bnj160 12485  bnj163OLD 12490  bnj168 12496  bnj512 12519  bnj542 12536  bnj551 12537  bnj559 12539  bnj880 12807  bnj937 12840  bnj1027 12882  bnj1072 12902  bnj1098 12917  bnj1159 12951  bnj1160 12952  bnj1182 12964  bnj1185 12967  bnj1192 12969  bnj1196 12972  bnj1201 12978  bnj1202 12979  bnj1211 12984  bnj1214 12988  bnj1278 13035  bnj1305 13048  bnj1322 13055  bnj1356 13081  bnj1369 13093  bnj1379 13100  bnj1397 13111  bnj1405 13115  bnj1406 13116  bnj1426 13120  bnj1437 13131  bnj1475 13152  bnj1476 13156  bnj1480 13157  bnj1506 13166  bnj1508 13168  bnj1531 13180  bnj1540 13187  bnj12 13194  bnj93 13217  bnj149 13241  bnj514 13255  bnj578 13291  bnj605 13292  bnj583 13296  bnj594 13300  bnj580 13301  bnj607 13304  bnj850 13312  bnj849 13318  bnj902 13326  bnj894 13327  bnj964 13347  bnj986 13360  bnj987 13361  bnj998 13363  bnj1052 13395  bnj1103 13415  bnj1108 13416  bnj1110 13417  bnj1121 13421  bnj1128 13428  bnj1284 13482  bnj1335 13503  bnj1388 13514  bnj1404 13517  bnj1417 13530  bnj1450 13541  bnj1529 13574  bnj1530 13575  elnn00nn 13602  ghomfo 13634  ghomgsg 13636  ghomf1olem 13637  cayleylem2 13642  suprzcl 13658  dvdsle 13693  alzdvds 13695  divalglem6 13701  divalglem8 13703  divalgb 13707  divalgmod 13709  ndvdssub 13710  gcdcllem1 13718  gcdcllem3 13720  eucalginv 13752  mulgcdlem2 13757  isprm3 13776  axpowprim 13788  axregprim 13789  trintOLD 13794  efrunt 13801  funpsstri 13835  elpotr 13847  dfon2lem4 13852  dfon2lem7 13855  distel 13870  predon 13904  tfisg 13912  wfi 13915  wfisg 13917  frind 13939  frinsg 13941  soxp 13950  frxp 13951  soseq 13955  wfr3g 13956  wfrlem4 13960  sltval2 13997  axdenselem3 14021  axdense 14027  axfelem0 14030  axfelem1 14031  axfelem3 14033  axfelem4 14034  axfelem5 14035  axfelem8 14038  axfelem9 14039  axfelem10 14040  axfelem11 14041  axfelem14 14044  altxpsspw 14100  waj-ax 14238  domfldrefc 14361  ranfldrefc 14362  eltids 14369  imfstnrelc 14396  cptwff 14436  fopab2g 14485  mapmapmap 14486  repcpwti 14503  dstr 14516  iscst4 14522  domrancur1b 14548  domrancur1c 14550  valcurfn 14551  domncnt 14624  ranncnt 14625  deref 14633  tostos 14637  fprodp1s 14682  fnopabco2b 14734  curgrpact 14735  trdom2 14755  svli2 14826  clsint 14860  cexint2 14862  hmphsyma 14882  hmphre 14884  hmeogrp 14892  homcard 14893  istopx 14918  efilcp 14922  filint2 14923  fgsb2 14925  efilcp2 14926  cnfilca 14927  dtt2 14951  cntrsetlem 14999  trdom 15013  cnvtr 15016  supbrr 15048  dualalg 15131  homib 15145  tarsuc1 15244  intartar 15255  vtarsuelt 15272  eltintpar 15276  ecase13d 15350  ioodisj 15364  elfiun 15369  inficlALT 15372  finsschain 15373  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem6OLD 15380  ordtypelem7OLD 15381  hartogOLD 15384  omsubsdomlem2OLD 15389  infenomsubOLD 15398  opncldf1 15402  opncldf3 15404  ntrcmp 15406  clscmp 15407  topbnd 15408  opnbnd 15409  ntrin 15411  clsun 15413  neiin 15418  subcls 15424  subntr 15425  cnsubsp 15426  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  reconnlem1 15446  reconnlem5 15450  reconn 15451  ivthALT 15454  2ndcctbss 15478  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop2lem4 15522  topmeet 15526  fnemeet1 15528  ist1-2 15542  fbasfip 15556  opnfbas 15557  filfinnfr 15561  filssufillem 15570  ufileu 15573  filufint 15574  uffixfr 15575  uffinfix 15577  ufinffr 15578  ufilen 15579  filcon 15580  ufcondr 15581  flimcls 15588  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfm 15598  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscomp 15621  tailf 15633  tailmap 15636  filnetlem1 15640  filnetlem3 15642  filnetlem5 15644  filnet 15645  cover2 15673  difin2 15676  resoprab2 15710  fnopabco 15711  mapfi 15727  upixp 15729  eropreu 15733  abrexdom 15739  fimax 15746  indexa 15753  indexfiOLD 15755  wofi 15770  frfi 15771  frminex 15773  fzm1 15796  sdclem1 15809  sdc 15811  fdc 15812  seqpo 15814  incsequz 15815  incsequz2 15816  nnubfi 15818  nninfnub 15819  fsum00 15820  fsumltisumii 15822  metf1o 15843  mettrifi 15847  geomcau 15849  lmclim2 15850  metdcn 15853  addccncf 15883  sub1cncf 15885  sub2cncf 15886  cnimass 15888  cnresima 15891  cnss 15892  hmeocnv 15898  sstotbnd 15936  isbnd3 15941  heiborlem1 15955  heiborlem11 15965  heiborlem16 15970  heiborlem23 15977  heiborlem31 15985  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  heiborlem41 15995  bfplem8 16005  rrnmet 16016  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  iccbnd 16026  exidreslem 16030  divrngcl 16110  isdivrng2 16111  isidlc 16163  divrngidl 16176  smprngpr 16200  igenval 16209  isfldidl 16216  prtlem90 16246  prtlem80 16247  erex 16262  erdisj3 16266  0nelqs2 16269  hgrablkne0 16295  sbeqal1 16355  ax10ext 16364  iotasbc 16383  pm14.12 16385  compne 16417  ralbidar 16422  rexbidar 16423  smoge 16454  eustrdif 16722  stb2val2 16736  stb3val2 16740  stb3val3 16741  stb2xpl 16742  stb3xpl 16743  pleval2 16785  pltn2lp 16789  cvrcmp 16999  hl1atom 17040  hlatmstc 17047  hlrelat2 17052  grpideuNEW 17114  divrngidNEW 17166  pmap0 17245  pmapsub 17250  pmapglb2 17253  pmapglb2x 17254  elpaddn0 17261  paddssat 17275  polat 17341  pnonsing 17343  osumcllem1 17364  osumcllem4 17367  osumcllem9 17372  osumcllem11 17374  pexmidlem6 17383  pexmidlem8 17385

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain