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  1610  nexd  1627  alexnim  1662  excomim  1677  19.41  1700  equcomd  1721  nfexd  1775  sbh  1790  sbcof2  1824  sbidm  1865  sb6rf  1867  nfsbt  1995  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  eu2  2089  2euex  2132  eqcomd  2202  3eltr3g  2281  abbid  2313  neneqd  2388  eqnetrrid  2398  3netr3g  2401  necomd  2453  r19.21bi  2585  nrexdv  2590  rexlimd  2611  rabbidva  2751  elisset  2777  euind  2951  rmoan  2964  reuind  2969  2rmorex  2970  spsbc  3001  spesbc  3075  eldifad  3168  eldifbd  3169  3sstr3g  3226  sseqtrdi  3232  difindiss  3418  un00  3498  undifss  3532  ifcldcd  3598  disjpr2  3687  difprsn1  3762  diftpsn3  3764  difsnss  3769  sneqr  3791  preqr1  3799  preq12b  3801  oprcl  3833  intab  3904  riinm  3990  rintm  4010  disjiun  4029  sndisj  4030  3brtr3g  4067  trint  4147  iinexgm  4188  exmidexmid  4230  exmid01  4232  pwntru  4233  exmid1stab  4242  pwel  4252  exss  4261  0nelop  4282  euotd  4288  opelopabsb  4295  pwunim  4322  issod  4355  frind  4388  suctr  4457  orduniss  4461  onelini  4466  oneluni  4467  eusv2i  4491  rexxfrd  4499  rabxfrd  4505  reuhypd  4507  iunpw  4516  sucexg  4535  ordsucim  4537  ordtriexmidlem  4556  ontriexmidim  4559  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsucunielexmid  4568  orddif  4584  suc11g  4594  onintexmid  4610  reg3exmidlemwe  4616  tfisi  4624  peano1  4631  peano2  4632  finds2  4638  omsinds  4659  brrelex12  4702  brel  4716  ssrel  4752  ssrel2  4754  ssrelrel  4764  elrel  4766  xpsspw  4776  relop  4817  dmxpm  4887  opelresi  4958  mptimass  5023  ndmima  5047  poirr2  5063  xpmlem  5091  xpimasn  5119  iotass  5237  iotacl  5244  dffun5r  5271  funeu  5284  funeu2  5285  funfnd  5290  funopg  5293  funun  5303  funinsn  5308  funtp  5312  funcnvuni  5328  funcnvres2  5334  imadiflem  5338  imadif  5339  funimaexglem  5342  fneu2  5366  fnimaeq0  5382  fnmpt  5387  fun2  5434  f00  5452  f0bi  5453  fimadmfo  5492  foimacnv  5525  resdif  5529  f1ococnv1  5536  fv3  5584  relelfvdm  5593  elfvm  5594  nfvres  5595  dffn5im  5609  mptfvex  5650  fvmptdf  5652  fvmptdv2  5654  fndmdif  5670  dff4im  5711  fmpt  5715  fmptd  5719  fmptdf  5722  f1oresrab  5730  fcoconst  5736  fsn  5737  ftpg  5749  fsnunf  5765  resfunexg  5786  isores1  5864  riota2df  5901  acexmidlemcase  5920  brabvv  5972  funoprabg  6025  fnovim  6035  ovmpodf  6058  ovi3  6064  elmpocl  6122  uchoice  6204  1stcof  6230  2ndcof  6231  fnmpo  6269  fmpoco  6283  fo2ndf  6294  f1o2ndf1  6295  disjxp1  6303  brtpos2  6318  reldmtpos  6320  dftpos3  6329  dftpos4  6330  tpostpos2  6332  tposf2  6335  tposf12  6336  tposfo  6338  tposf  6339  smores2  6361  tfrlem1  6375  tfrlem3-2d  6379  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemi1  6399  tfrexlem  6401  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcldm  6430  rdgivallem  6448  rdgisucinc  6452  frecabex  6465  frecfnom  6468  frecfcllem  6471  frecsuclem  6473  omsuc  6539  nntri2  6561  nnsucuniel  6562  nnsseleq  6568  nnm00  6597  ecexr  6606  swoer  6629  elqsn0m  6671  iinerm  6675  erinxp  6677  ecinxp  6678  eroveu  6694  eroprf  6696  mapprc  6720  mapsn  6758  ixpprc  6787  ixp0  6799  resixp  6801  elixpsn  6803  dom2lem  6840  fundmen  6874  dom0  6908  xpf1o  6914  mapxpen  6918  xpmapenlem  6919  ssenen  6921  nneneq  6927  ssfilem  6945  dif1en  6949  dif1enen  6950  fin0  6955  fin0or  6956  diffitest  6957  diffisn  6963  ac6sfi  6968  fimax2gtrilemstep  6970  fimax2gtri  6971  finexdc  6972  exmidpweq  6979  pw1fin  6980  onunsnss  6987  unsnfidcel  6991  undifdcss  6993  undifdc  6994  tpfidceq  7000  fiintim  7001  fisseneq  7004  fidcenumlemr  7030  sbthlemi4  7035  sbthlemi5  7036  sbthlemi9  7040  fifo  7055  suplubti  7075  supelti  7077  infmoti  7103  infisoti  7107  djulclb  7130  updjud  7157  omp1eomlem  7169  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumct  7190  nninfninc  7198  nnnninfeq2  7204  finomni  7215  fodjuomnilemdc  7219  fodjum  7221  fodjuomnilemres  7223  fodjumkvlemres  7234  omniwomnimkv  7242  nninfwlporlem  7248  nninfwlpoimlemginf  7251  nninfwlpoim  7253  ficardon  7267  exmidonfinlem  7272  en2eleq  7274  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  exmidfodomrlemim  7280  finacn  7287  acfun  7290  exmidaclem  7291  exmidontriimlem3  7306  exmidontriimlem4  7307  exmidontriim  7308  pw1on  7309  dftap2  7334  2omotaplemst  7341  exmidapne  7343  ccfunen  7347  cc1  7348  cc2lem  7349  cc2  7350  cc3  7351  acnccim  7355  elni2  7398  indpi  7426  distrnqg  7471  subhalfnqq  7498  enq0sym  7516  enq0ref  7517  enq0tr  7518  nqnq0pi  7522  nnnq0lem1  7530  distrnq0  7543  elinp  7558  elnp1st2nd  7560  prltlu  7571  prnmaxl  7572  prnminu  7573  prarloc  7587  nqprm  7626  appdivnq  7647  prmuloc  7650  mullocpr  7655  distrlem4prl  7668  distrlem4pru  7669  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  cauappcvgprlemopl  7730  cauappcvgprlemopu  7732  cauappcvgprlemdisj  7735  cauappcvgprlem2  7744  cauappcvgprlemlim  7745  caucvgprlemnkj  7750  caucvgprlemopl  7753  caucvgprlemopu  7755  caucvgprlemdisj  7758  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem2  7764  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemlol  7782  caucvgprprlemexbt  7790  caucvgprprlem1  7793  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  prsrlem1  7826  gt0srpr  7832  caucvgsrlemcl  7873  caucvgsrlembound  7878  caucvgsrlemgt1  7879  suplocsrlemb  7890  suplocsrlem  7892  suplocsr  7893  ltresr  7923  nnindnn  7977  axcaucvglemcl  7979  axcaucvglemval  7981  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  sup3exmid  9001  nnind  9023  nn0supp  9318  nn0ge2m1nn  9326  zleloe  9390  zapne  9417  nn0lt2  9424  suprzclex  9441  zindd  9461  uzm1  9649  uzin  9651  infregelbex  9689  elnn1uz2  9698  nn01to3  9708  divfnzn  9712  qapne  9730  xrltnsym2  9886  xaddass  9961  xleadd1a  9965  xlt2add  9972  xlesubadd  9975  iooval2  10007  icoshftf1o  10083  fztri3or  10131  fzneuz  10193  4fvwrd4  10232  elfzo0  10275  infssuzex  10340  infssuzcldc  10342  suprzubdc  10343  nninfdcex  10344  zsupssdc  10345  exbtwnzlemex  10356  ioom  10367  fzfig  10539  uzennn  10545  uzsinds  10553  iseqovex  10567  seq3val  10569  seqvalcd  10570  seqf  10573  seqovcd  10576  monoord2  10595  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  seq3f1olemqsum  10622  seq3f1o  10626  seqf1og  10630  seq3distr  10641  expp1  10655  expcl2lemap  10660  expclzap  10673  expap0i  10680  nn0ltexp2  10818  bcval5  10872  hashinfuni  10886  hashennnuni  10888  hashnncl  10904  resunimafz0  10940  zfz1isolemiso  10948  zfz1isolem1  10949  zfz1iso  10950  wrdsymb0  10984  wrdlen1  10989  seq3shft  11020  cvg1nlemcau  11166  rexanuz  11170  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  rersqreu  11210  caubnd2  11299  maxleast  11395  fimaxre2  11409  minmax  11412  xrmaxiflemcl  11427  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxadd  11443  xrminmax  11447  xrbdtri  11458  climreu  11479  reccn2ap  11495  iserex  11521  climcvg1nlem  11531  serf0  11534  fz1f1o  11557  summodclem3  11562  zsumdc  11566  fsum3  11569  isumz  11571  isumss  11573  isumss2  11575  fsumsersdc  11577  fsum3ser  11579  fsumsplit  11589  isumclim2  11604  isumclim3  11605  fsum2dlemstep  11616  fsumcnv  11619  fisumcom2  11620  bcxmas  11671  isumle  11677  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratz  11714  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  zproddc  11761  prod1dc  11768  fprodsplitdc  11778  fprodsplit  11779  fprodunsn  11786  fprodcl2lem  11787  fprodcllemf  11795  fprod2dlemstep  11804  fprodcnv  11807  fprodcom2fi  11808  fprodle  11822  ef0lem  11842  fsumdvds  12024  mod2eq1n2dvds  12061  ndvdssub  12112  bitsfzolem  12136  bitsfzo  12137  bitsinv1  12144  gcdsupex  12149  gcdsupcl  12150  bezoutlemnewy  12188  bezoutlemmain  12190  bezoutlembi  12197  bezoutlemeu  12199  bezoutlemle  12200  uzwodc  12229  nnwofdc  12230  nnwosdc  12231  nninfctlemfo  12232  nninfct  12233  nn0seqcvgd  12234  eucalgf  12248  eucalginv  12249  lcmval  12256  prmind2  12313  dfphi2  12413  phiprmpw  12415  phimullem  12418  eulerthlem1  12420  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  eulerth  12426  phisum  12434  odzcllem  12436  odzdvds  12439  pythagtriplem19  12476  pclemub  12481  pcprecl  12483  pceu  12489  pcqmul  12497  pcqcl  12500  pcxnn0cl  12504  pcxqcl  12506  pcge0  12507  pcdvdsb  12514  pceq0  12516  pcneg  12519  pcdvdstr  12521  pcgcd1  12522  pc2dvds  12524  pcz  12526  pcprmpw2  12527  pcaddlem  12533  pcadd  12534  pcmptcl  12536  pcmpt  12537  pcmptdvds  12539  fldivp1  12542  qexpz  12546  pockthlem  12550  pockthg  12551  prmunb  12556  1arith  12561  4sqlemffi  12590  4sqlem17  12601  4sqlem18  12602  4sqlem19  12603  ennnfonelemom  12650  ennnfoneleminc  12653  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemdm  12662  ennnfonelemr  12665  ennnfonelemim  12666  exmidunben  12668  ctinfom  12670  inffinp1  12671  ctinf  12672  enctlem  12674  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  ctiunctlemudc  12679  ctiunct  12682  ctiunctal  12683  unct  12684  ssomct  12687  nninfdclemcl  12690  nninfdclemp1  12692  nninfdc  12695  structcnvcnv  12719  setscom  12743  relelbasov  12765  ressbas2d  12771  ressval3d  12775  ressabsg  12779  restid2  12950  imasaddfnlemg  13016  quslem  13026  ercpbl  13033  fnpr2ob  13042  mgmplusf  13068  grpinvalem  13087  grpinva  13088  grprida  13089  fngsum  13090  igsumvalx  13091  gsum0g  13098  gsumval2  13099  ismnd  13121  mhmpropd  13168  grppropd  13219  grpsubf  13281  dfgrp3mlem  13300  mulgnn0p1  13339  mulgnn0subcl  13341  mulgsubcl  13342  mulgneg  13346  mulgnn0dir  13358  mulgnn0ass  13364  submmulg  13372  issubg2m  13395  issubg4m  13399  ghmmulg  13462  ghmrn  13463  lringuplu  13828  lmodscaf  13942  lssintclm  14016  lspun0  14057  lidlbas  14110  psr1clfi  14316  topontopon  14340  eltg3i  14376  epttop  14410  difopn  14428  uncld  14433  0nnei  14473  resttopon  14491  restabs  14495  restopnb  14501  lmcvg  14537  cnptopco  14542  cnss1  14546  cnss2  14547  cncnpi  14548  cncnp2m  14551  cnrest  14555  cnrest2  14556  cnrest2r  14557  cnptoprest  14559  cnptoprest2  14560  lmss  14566  lmff  14569  lmtopcnp  14570  lmcn  14571  txbasval  14587  upxp  14592  txcnmpt  14593  txdis1cn  14598  txlm  14599  lmcn2  14600  cnmpt11  14603  cnmpt11f  14604  cnmpt1t  14605  cnmpt12  14607  cnmpt21  14611  cnmpt21f  14612  cnmpt2t  14613  cnmpt22  14614  cnmpt22f  14615  cnmptcom  14618  hmeocnv  14627  hmeof1o  14629  hmeores  14635  txhmeo  14639  txswaphmeo  14641  isxmet2d  14668  blfvalps  14705  xblss2ps  14724  xblss2  14725  blfps  14729  blf  14730  unirnblps  14742  unirnbl  14743  isxms2  14772  bdxmet  14821  bdmet  14822  xmetxp  14827  xmettx  14830  blssioo  14873  tgioo  14874  mulcncflem  14927  divcncfap  14934  dedekindeulemuub  14937  dedekindeulemub  14938  dedekindeulemloc  14939  dedekindeulemlu  14941  suplociccreex  14944  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemub  14947  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthdich  14973  limcrcl  14978  limcmpted  14983  limccnp2lem  14996  limccnp2cntop  14997  limccoap  14998  dvrecap  15033  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  plyco  15079  plycj  15081  plyrecj  15083  dvply1  15085  dvply2g  15086  cosordlem  15169  logbgcd1irraplemexp  15288  logbgcd1irrap  15290  lgsneg1  15350  lgsdilem  15352  lgsdir2  15358  lgsdirprm  15359  lgsdir  15360  lgsne0  15363  lgsabs1  15364  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1f1o  15385  gausslemma2dlem4  15389  lgseisenlem1  15395  lgsquadlem3  15404  2lgslem1a  15413  2sqlem5  15444  2sqlem7  15446  2sqlem8a  15447  2sqlem8  15448  2sqlem9  15449  bj-stand  15478  bj-charfundcALT  15539  bj-charfunbi  15541  bj-bdfindis  15677  bj-peano4  15685  strcollnfALT  15716  1dom1el  15721  2omap  15726  pwtrufal  15728  pwf1oexmid  15730  subctctexmid  15731  pw1nct  15734  nnsf  15736  nninfalllem1  15739  nninfall  15740  nninfsellemqall  15746  nnnninfen  15752  exmidsbthrlem  15753  sbthom  15757  cvgcmp2nlemabs  15763  trilpo  15774  iswomni0  15782  redcwlpo  15786  dceqnconst  15791  dcapnconst  15792  nconstwlpolem  15796  nconstwlpo  15797  neapmkvlem  15798  neapmkv  15799  ltlenmkv  15801  taupi  15804  alsi1d  15812  alsi2d  15813  alsc1d  15814  alsc2d  15815