Theorem sylib 122

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.)

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 120	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb1  137  bicomd  141  pm5.74d  182  bitri  184  3imtr3i  200  ancomd  267  pm4.71d  393  pm4.71rd  394  imdistand  447  orcomd  730  3mix3  1170  mpjao3dan  1318  ecase23d  1361  exlimdh  1607  nexd  1624  alexnim  1659  excomim  1674  19.41  1697  equcomd  1718  nfexd  1772  sbh  1787  sbcof2  1821  sbidm  1862  sb6rf  1864  nfsbt  1992  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  eu2  2086  2euex  2129  eqcomd  2199  3eltr3g  2278  abbid  2310  neneqd  2385  eqnetrrid  2395  3netr3g  2398  necomd  2450  r19.21bi  2582  nrexdv  2587  rexlimd  2608  rabbidva  2748  elisset  2774  euind  2947  rmoan  2960  reuind  2965  2rmorex  2966  spsbc  2997  spesbc  3071  eldifad  3164  eldifbd  3165  3sstr3g  3221  sseqtrdi  3227  difindiss  3413  un00  3493  undifss  3527  ifcldcd  3593  disjpr2  3682  difprsn1  3757  diftpsn3  3759  difsnss  3764  sneqr  3786  preqr1  3794  preq12b  3796  oprcl  3828  intab  3899  riinm  3985  rintm  4005  disjiun  4024  sndisj  4025  3brtr3g  4062  trint  4142  iinexgm  4183  exmidexmid  4225  exmid01  4227  pwntru  4228  exmid1stab  4237  pwel  4247  exss  4256  0nelop  4277  euotd  4283  opelopabsb  4290  pwunim  4317  issod  4350  frind  4383  suctr  4452  orduniss  4456  onelini  4461  oneluni  4462  eusv2i  4486  rexxfrd  4494  rabxfrd  4500  reuhypd  4502  iunpw  4511  sucexg  4530  ordsucim  4532  ordtriexmidlem  4551  ontriexmidim  4554  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  ordsucunielexmid  4563  orddif  4579  suc11g  4589  onintexmid  4605  reg3exmidlemwe  4611  tfisi  4619  peano1  4626  peano2  4627  finds2  4633  omsinds  4654  brrelex12  4697  brel  4711  ssrel  4747  ssrel2  4749  ssrelrel  4759  elrel  4761  xpsspw  4771  relop  4812  dmxpm  4882  opelresi  4953  mptimass  5018  ndmima  5042  poirr2  5058  xpmlem  5086  xpimasn  5114  iotass  5232  iotacl  5239  dffun5r  5266  funeu  5279  funeu2  5280  funfnd  5285  funopg  5288  funun  5298  funinsn  5303  funtp  5307  funcnvuni  5323  funcnvres2  5329  imadiflem  5333  imadif  5334  funimaexglem  5337  fneu2  5359  fnimaeq0  5375  fnmpt  5380  fun2  5427  f00  5445  f0bi  5446  fimadmfo  5485  foimacnv  5518  resdif  5522  f1ococnv1  5529  fv3  5577  relelfvdm  5586  elfvm  5587  nfvres  5588  dffn5im  5602  mptfvex  5643  fvmptdf  5645  fvmptdv2  5647  fndmdif  5663  dff4im  5704  fmpt  5708  fmptd  5712  fmptdf  5715  f1oresrab  5723  fcoconst  5729  fsn  5730  ftpg  5742  fsnunf  5758  resfunexg  5779  isores1  5857  riota2df  5894  acexmidlemcase  5913  brabvv  5964  funoprabg  6017  fnovim  6027  ovmpodf  6050  ovi3  6055  elmpocl  6113  uchoice  6190  1stcof  6216  2ndcof  6217  fnmpo  6255  fmpoco  6269  fo2ndf  6280  f1o2ndf1  6281  disjxp1  6289  brtpos2  6304  reldmtpos  6306  dftpos3  6315  dftpos4  6316  tpostpos2  6318  tposf2  6321  tposf12  6322  tposfo  6324  tposf  6325  smores2  6347  tfrlem1  6361  tfrlem3-2d  6365  tfrlemisucaccv  6378  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrlemi1  6385  tfrexlem  6387  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  tfrcldm  6416  rdgivallem  6434  rdgisucinc  6438  frecabex  6451  frecfnom  6454  frecfcllem  6457  frecsuclem  6459  omsuc  6525  nntri2  6547  nnsucuniel  6548  nnsseleq  6554  nnm00  6583  ecexr  6592  swoer  6615  elqsn0m  6657  iinerm  6661  erinxp  6663  ecinxp  6664  eroveu  6680  eroprf  6682  mapprc  6706  mapsn  6744  ixpprc  6773  ixp0  6785  resixp  6787  elixpsn  6789  dom2lem  6826  fundmen  6860  dom0  6894  xpf1o  6900  mapxpen  6904  xpmapenlem  6905  ssenen  6907  nneneq  6913  ssfilem  6931  dif1en  6935  dif1enen  6936  fin0  6941  fin0or  6942  diffitest  6943  diffisn  6949  ac6sfi  6954  fimax2gtrilemstep  6956  fimax2gtri  6957  finexdc  6958  exmidpweq  6965  pw1fin  6966  onunsnss  6973  unsnfidcel  6977  undifdcss  6979  undifdc  6980  fiintim  6985  fisseneq  6988  fidcenumlemr  7014  sbthlemi4  7019  sbthlemi5  7020  sbthlemi9  7024  fifo  7039  suplubti  7059  supelti  7061  infmoti  7087  infisoti  7091  djulclb  7114  updjud  7141  omp1eomlem  7153  0ct  7166  ctmlemr  7167  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  enumct  7174  nninfninc  7182  nnnninfeq2  7188  finomni  7199  fodjuomnilemdc  7203  fodjum  7205  fodjuomnilemres  7207  fodjumkvlemres  7218  omniwomnimkv  7226  nninfwlporlem  7232  nninfwlpoimlemginf  7235  nninfwlpoim  7237  exmidonfinlem  7253  en2eleq  7255  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  exmidfodomrlemim  7261  acfun  7267  exmidaclem  7268  exmidontriimlem3  7283  exmidontriimlem4  7284  exmidontriim  7285  pw1on  7286  dftap2  7311  2omotaplemst  7318  exmidapne  7320  ccfunen  7324  cc1  7325  cc2lem  7326  cc2  7327  cc3  7328  elni2  7374  indpi  7402  distrnqg  7447  subhalfnqq  7474  enq0sym  7492  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  nnnq0lem1  7506  distrnq0  7519  elinp  7534  elnp1st2nd  7536  prltlu  7547  prnmaxl  7548  prnminu  7549  prarloc  7563  nqprm  7602  appdivnq  7623  prmuloc  7626  mullocpr  7631  distrlem4prl  7644  distrlem4pru  7645  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  cauappcvgprlemopl  7706  cauappcvgprlemopu  7708  cauappcvgprlemdisj  7711  cauappcvgprlem2  7720  cauappcvgprlemlim  7721  caucvgprlemnkj  7726  caucvgprlemopl  7729  caucvgprlemopu  7731  caucvgprlemdisj  7734  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem2  7740  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemlol  7758  caucvgprprlemexbt  7766  caucvgprprlem1  7769  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  prsrlem1  7802  gt0srpr  7808  caucvgsrlemcl  7849  caucvgsrlembound  7854  caucvgsrlemgt1  7855  suplocsrlemb  7866  suplocsrlem  7868  suplocsr  7869  ltresr  7899  nnindnn  7953  axcaucvglemcl  7955  axcaucvglemval  7957  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  sup3exmid  8976  nnind  8998  nn0supp  9292  nn0ge2m1nn  9300  zleloe  9364  zapne  9391  nn0lt2  9398  suprzclex  9415  zindd  9435  uzm1  9623  uzin  9625  infregelbex  9663  elnn1uz2  9672  nn01to3  9682  divfnzn  9686  qapne  9704  xrltnsym2  9860  xaddass  9935  xleadd1a  9939  xlt2add  9946  xlesubadd  9949  iooval2  9981  icoshftf1o  10057  fztri3or  10105  fzneuz  10167  4fvwrd4  10206  elfzo0  10249  exbtwnzlemex  10318  ioom  10329  fzfig  10501  uzennn  10507  uzsinds  10515  iseqovex  10529  seq3val  10531  seqvalcd  10532  seqf  10535  seqovcd  10538  monoord2  10557  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seq3f1olemqsum  10584  seq3f1o  10588  seqf1og  10592  seq3distr  10603  expp1  10617  expcl2lemap  10622  expclzap  10635  expap0i  10642  nn0ltexp2  10780  bcval5  10834  hashinfuni  10848  hashennnuni  10850  hashnncl  10866  resunimafz0  10902  zfz1isolemiso  10910  zfz1isolem1  10911  zfz1iso  10912  wrdsymb0  10946  wrdlen1  10951  seq3shft  10982  cvg1nlemcau  11128  rexanuz  11132  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  rersqreu  11172  caubnd2  11261  maxleast  11357  fimaxre2  11370  minmax  11373  xrmaxiflemcl  11388  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxadd  11404  xrminmax  11408  xrbdtri  11419  climreu  11440  reccn2ap  11456  iserex  11482  climcvg1nlem  11492  serf0  11495  fz1f1o  11518  summodclem3  11523  zsumdc  11527  fsum3  11530  isumz  11532  isumss  11534  isumss2  11536  fsumsersdc  11538  fsum3ser  11540  fsumsplit  11550  isumclim2  11565  isumclim3  11566  fsum2dlemstep  11577  fsumcnv  11580  fisumcom2  11581  bcxmas  11632  isumle  11638  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratz  11675  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  zproddc  11722  prod1dc  11729  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  fprodcl2lem  11748  fprodcllemf  11756  fprod2dlemstep  11765  fprodcnv  11768  fprodcom2fi  11769  fprodle  11783  ef0lem  11803  mod2eq1n2dvds  12020  ndvdssub  12071  infssuzex  12086  infssuzcldc  12088  suprzubdc  12089  nninfdcex  12090  zsupssdc  12091  gcdsupex  12094  gcdsupcl  12095  bezoutlemnewy  12133  bezoutlemmain  12135  bezoutlembi  12142  bezoutlemeu  12144  bezoutlemle  12145  uzwodc  12174  nnwofdc  12175  nnwosdc  12176  nninfctlemfo  12177  nninfct  12178  nn0seqcvgd  12179  eucalgf  12193  eucalginv  12194  lcmval  12201  prmind2  12258  dfphi2  12358  phiprmpw  12360  phimullem  12363  eulerthlem1  12365  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  eulerth  12371  phisum  12378  odzcllem  12380  odzdvds  12383  pythagtriplem19  12420  pclemub  12425  pcprecl  12427  pceu  12433  pcqmul  12441  pcqcl  12444  pcxnn0cl  12448  pcxqcl  12450  pcge0  12451  pcdvdsb  12458  pceq0  12460  pcneg  12463  pcdvdstr  12465  pcgcd1  12466  pc2dvds  12468  pcz  12470  pcprmpw2  12471  pcaddlem  12477  pcadd  12478  pcmptcl  12480  pcmpt  12481  pcmptdvds  12483  fldivp1  12486  qexpz  12490  pockthlem  12494  pockthg  12495  prmunb  12500  1arith  12505  4sqlemffi  12534  4sqlem17  12545  4sqlem18  12546  4sqlem19  12547  ennnfonelemom  12565  ennnfoneleminc  12568  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemdm  12577  ennnfonelemr  12580  ennnfonelemim  12581  exmidunben  12583  ctinfom  12585  inffinp1  12586  ctinf  12587  enctlem  12589  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  ctiunctlemudc  12594  ctiunct  12597  ctiunctal  12598  unct  12599  ssomct  12602  nninfdclemcl  12605  nninfdclemp1  12607  nninfdc  12610  structcnvcnv  12634  setscom  12658  relelbasov  12680  ressbas2d  12686  ressval3d  12690  ressabsg  12694  restid2  12859  imasaddfnlemg  12897  quslem  12907  ercpbl  12914  fnpr2ob  12923  mgmplusf  12949  grpinvalem  12968  grpinva  12969  grprida  12970  fngsum  12971  igsumvalx  12972  gsum0g  12979  gsumval2  12980  ismnd  13000  mhmpropd  13038  grppropd  13089  grpsubf  13151  dfgrp3mlem  13170  mulgnn0p1  13203  mulgnn0subcl  13205  mulgsubcl  13206  mulgneg  13210  mulgnn0dir  13222  mulgnn0ass  13228  submmulg  13236  issubg2m  13259  issubg4m  13263  ghmmulg  13326  ghmrn  13327  lringuplu  13692  lmodscaf  13806  lssintclm  13880  lspun0  13921  lidlbas  13974  topontopon  14188  eltg3i  14224  epttop  14258  difopn  14276  uncld  14281  0nnei  14321  resttopon  14339  restabs  14343  restopnb  14349  lmcvg  14385  cnptopco  14390  cnss1  14394  cnss2  14395  cncnpi  14396  cncnp2m  14399  cnrest  14403  cnrest2  14404  cnrest2r  14405  cnptoprest  14407  cnptoprest2  14408  lmss  14414  lmff  14417  lmtopcnp  14418  lmcn  14419  txbasval  14435  upxp  14440  txcnmpt  14441  txdis1cn  14446  txlm  14447  lmcn2  14448  cnmpt11  14451  cnmpt11f  14452  cnmpt1t  14453  cnmpt12  14455  cnmpt21  14459  cnmpt21f  14460  cnmpt2t  14461  cnmpt22  14462  cnmpt22f  14463  cnmptcom  14466  hmeocnv  14475  hmeof1o  14477  hmeores  14483  txhmeo  14487  txswaphmeo  14489  isxmet2d  14516  blfvalps  14553  xblss2ps  14572  xblss2  14573  blfps  14577  blf  14578  unirnblps  14590  unirnbl  14591  isxms2  14620  bdxmet  14669  bdmet  14670  xmetxp  14675  xmettx  14678  blssioo  14713  tgioo  14714  mulcncflem  14761  divcncfap  14768  dedekindeulemuub  14771  dedekindeulemub  14772  dedekindeulemloc  14773  dedekindeulemlu  14775  suplociccreex  14778  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemub  14781  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthdich  14807  limcrcl  14812  limcmpted  14817  limccnp2lem  14830  limccnp2cntop  14831  limccoap  14832  dvrecap  14862  plyaddlem1  14893  plymullem1  14894  cosordlem  14984  logbgcd1irraplemexp  15100  logbgcd1irrap  15102  lgsneg1  15141  lgsdilem  15143  lgsdir2  15149  lgsdirprm  15150  lgsdir  15151  lgsne0  15154  lgsabs1  15155  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1f1o  15176  gausslemma2dlem4  15180  lgseisenlem1  15186  2sqlem5  15206  2sqlem7  15208  2sqlem8a  15209  2sqlem8  15210  2sqlem9  15211  bj-stand  15240  bj-charfundcALT  15301  bj-charfunbi  15303  bj-bdfindis  15439  bj-peano4  15447  strcollnfALT  15478  1dom1el  15483  pwtrufal  15488  pwf1oexmid  15490  subctctexmid  15491  pw1nct  15493  nnsf  15495  nninfalllem1  15498  nninfall  15499  nninfsellemqall  15505  nnnninfen  15511  exmidsbthrlem  15512  sbthom  15516  cvgcmp2nlemabs  15522  trilpo  15533  iswomni0  15541  redcwlpo  15545  dceqnconst  15550  dcapnconst  15551  nconstwlpolem  15555  nconstwlpo  15556  neapmkvlem  15557  neapmkv  15558  ltlenmkv  15560  taupi  15563  alsi1d  15571  alsi2d  15572  alsc1d  15573  alsc2d  15574