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  3225  sseqtrdi  3231  difindiss  3417  un00  3497  undifss  3531  ifcldcd  3597  disjpr2  3686  difprsn1  3761  diftpsn3  3763  difsnss  3768  sneqr  3790  preqr1  3798  preq12b  3800  oprcl  3832  intab  3903  riinm  3989  rintm  4009  disjiun  4028  sndisj  4029  3brtr3g  4066  trint  4146  iinexgm  4187  exmidexmid  4229  exmid01  4231  pwntru  4232  exmid1stab  4241  pwel  4251  exss  4260  0nelop  4281  euotd  4287  opelopabsb  4294  pwunim  4321  issod  4354  frind  4387  suctr  4456  orduniss  4460  onelini  4465  oneluni  4466  eusv2i  4490  rexxfrd  4498  rabxfrd  4504  reuhypd  4506  iunpw  4515  sucexg  4534  ordsucim  4536  ordtriexmidlem  4555  ontriexmidim  4558  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  ordsucunielexmid  4567  orddif  4583  suc11g  4593  onintexmid  4609  reg3exmidlemwe  4615  tfisi  4623  peano1  4630  peano2  4631  finds2  4637  omsinds  4658  brrelex12  4701  brel  4715  ssrel  4751  ssrel2  4753  ssrelrel  4763  elrel  4765  xpsspw  4775  relop  4816  dmxpm  4886  opelresi  4957  mptimass  5022  ndmima  5046  poirr2  5062  xpmlem  5090  xpimasn  5118  iotass  5236  iotacl  5243  dffun5r  5270  funeu  5283  funeu2  5284  funfnd  5289  funopg  5292  funun  5302  funinsn  5307  funtp  5311  funcnvuni  5327  funcnvres2  5333  imadiflem  5337  imadif  5338  funimaexglem  5341  fneu2  5363  fnimaeq0  5379  fnmpt  5384  fun2  5431  f00  5449  f0bi  5450  fimadmfo  5489  foimacnv  5522  resdif  5526  f1ococnv1  5533  fv3  5581  relelfvdm  5590  elfvm  5591  nfvres  5592  dffn5im  5606  mptfvex  5647  fvmptdf  5649  fvmptdv2  5651  fndmdif  5667  dff4im  5708  fmpt  5712  fmptd  5716  fmptdf  5719  f1oresrab  5727  fcoconst  5733  fsn  5734  ftpg  5746  fsnunf  5762  resfunexg  5783  isores1  5861  riota2df  5898  acexmidlemcase  5917  brabvv  5968  funoprabg  6021  fnovim  6031  ovmpodf  6054  ovi3  6060  elmpocl  6118  uchoice  6195  1stcof  6221  2ndcof  6222  fnmpo  6260  fmpoco  6274  fo2ndf  6285  f1o2ndf1  6286  disjxp1  6294  brtpos2  6309  reldmtpos  6311  dftpos3  6320  dftpos4  6321  tpostpos2  6323  tposf2  6326  tposf12  6327  tposfo  6329  tposf  6330  smores2  6352  tfrlem1  6366  tfrlem3-2d  6370  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrlemi1  6390  tfrexlem  6392  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  tfrcldm  6421  rdgivallem  6439  rdgisucinc  6443  frecabex  6456  frecfnom  6459  frecfcllem  6462  frecsuclem  6464  omsuc  6530  nntri2  6552  nnsucuniel  6553  nnsseleq  6559  nnm00  6588  ecexr  6597  swoer  6620  elqsn0m  6662  iinerm  6666  erinxp  6668  ecinxp  6669  eroveu  6685  eroprf  6687  mapprc  6711  mapsn  6749  ixpprc  6778  ixp0  6790  resixp  6792  elixpsn  6794  dom2lem  6831  fundmen  6865  dom0  6899  xpf1o  6905  mapxpen  6909  xpmapenlem  6910  ssenen  6912  nneneq  6918  ssfilem  6936  dif1en  6940  dif1enen  6941  fin0  6946  fin0or  6947  diffitest  6948  diffisn  6954  ac6sfi  6959  fimax2gtrilemstep  6961  fimax2gtri  6962  finexdc  6963  exmidpweq  6970  pw1fin  6971  onunsnss  6978  unsnfidcel  6982  undifdcss  6984  undifdc  6985  tpfidceq  6991  fiintim  6992  fisseneq  6995  fidcenumlemr  7021  sbthlemi4  7026  sbthlemi5  7027  sbthlemi9  7031  fifo  7046  suplubti  7066  supelti  7068  infmoti  7094  infisoti  7098  djulclb  7121  updjud  7148  omp1eomlem  7160  0ct  7173  ctmlemr  7174  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumct  7181  nninfninc  7189  nnnninfeq2  7195  finomni  7206  fodjuomnilemdc  7210  fodjum  7212  fodjuomnilemres  7214  fodjumkvlemres  7225  omniwomnimkv  7233  nninfwlporlem  7239  nninfwlpoimlemginf  7242  nninfwlpoim  7244  exmidonfinlem  7260  en2eleq  7262  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  exmidfodomrlemim  7268  acfun  7274  exmidaclem  7275  exmidontriimlem3  7290  exmidontriimlem4  7291  exmidontriim  7292  pw1on  7293  dftap2  7318  2omotaplemst  7325  exmidapne  7327  ccfunen  7331  cc1  7332  cc2lem  7333  cc2  7334  cc3  7335  elni2  7381  indpi  7409  distrnqg  7454  subhalfnqq  7481  enq0sym  7499  enq0ref  7500  enq0tr  7501  nqnq0pi  7505  nnnq0lem1  7513  distrnq0  7526  elinp  7541  elnp1st2nd  7543  prltlu  7554  prnmaxl  7555  prnminu  7556  prarloc  7570  nqprm  7609  appdivnq  7630  prmuloc  7633  mullocpr  7638  distrlem4prl  7651  distrlem4pru  7652  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  cauappcvgprlemopl  7713  cauappcvgprlemopu  7715  cauappcvgprlemdisj  7718  cauappcvgprlem2  7727  cauappcvgprlemlim  7728  caucvgprlemnkj  7733  caucvgprlemopl  7736  caucvgprlemopu  7738  caucvgprlemdisj  7741  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem2  7747  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemlol  7765  caucvgprprlemexbt  7773  caucvgprprlem1  7776  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  prsrlem1  7809  gt0srpr  7815  caucvgsrlemcl  7856  caucvgsrlembound  7861  caucvgsrlemgt1  7862  suplocsrlemb  7873  suplocsrlem  7875  suplocsr  7876  ltresr  7906  nnindnn  7960  axcaucvglemcl  7962  axcaucvglemval  7964  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  sup3exmid  8984  nnind  9006  nn0supp  9301  nn0ge2m1nn  9309  zleloe  9373  zapne  9400  nn0lt2  9407  suprzclex  9424  zindd  9444  uzm1  9632  uzin  9634  infregelbex  9672  elnn1uz2  9681  nn01to3  9691  divfnzn  9695  qapne  9713  xrltnsym2  9869  xaddass  9944  xleadd1a  9948  xlt2add  9955  xlesubadd  9958  iooval2  9990  icoshftf1o  10066  fztri3or  10114  fzneuz  10176  4fvwrd4  10215  elfzo0  10258  infssuzex  10323  infssuzcldc  10325  suprzubdc  10326  nninfdcex  10327  zsupssdc  10328  exbtwnzlemex  10339  ioom  10350  fzfig  10522  uzennn  10528  uzsinds  10536  iseqovex  10550  seq3val  10552  seqvalcd  10553  seqf  10556  seqovcd  10559  monoord2  10578  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  seq3f1olemqsum  10605  seq3f1o  10609  seqf1og  10613  seq3distr  10624  expp1  10638  expcl2lemap  10643  expclzap  10656  expap0i  10663  nn0ltexp2  10801  bcval5  10855  hashinfuni  10869  hashennnuni  10871  hashnncl  10887  resunimafz0  10923  zfz1isolemiso  10931  zfz1isolem1  10932  zfz1iso  10933  wrdsymb0  10967  wrdlen1  10972  seq3shft  11003  cvg1nlemcau  11149  rexanuz  11153  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  rersqreu  11193  caubnd2  11282  maxleast  11378  fimaxre2  11392  minmax  11395  xrmaxiflemcl  11410  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxadd  11426  xrminmax  11430  xrbdtri  11441  climreu  11462  reccn2ap  11478  iserex  11504  climcvg1nlem  11514  serf0  11517  fz1f1o  11540  summodclem3  11545  zsumdc  11549  fsum3  11552  isumz  11554  isumss  11556  isumss2  11558  fsumsersdc  11560  fsum3ser  11562  fsumsplit  11572  isumclim2  11587  isumclim3  11588  fsum2dlemstep  11599  fsumcnv  11602  fisumcom2  11603  bcxmas  11654  isumle  11660  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratz  11697  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  zproddc  11744  prod1dc  11751  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  fprodcl2lem  11770  fprodcllemf  11778  fprod2dlemstep  11787  fprodcnv  11790  fprodcom2fi  11791  fprodle  11805  ef0lem  11825  fsumdvds  12007  mod2eq1n2dvds  12044  ndvdssub  12095  bitsfzolem  12118  bitsfzo  12119  gcdsupex  12124  gcdsupcl  12125  bezoutlemnewy  12163  bezoutlemmain  12165  bezoutlembi  12172  bezoutlemeu  12174  bezoutlemle  12175  uzwodc  12204  nnwofdc  12205  nnwosdc  12206  nninfctlemfo  12207  nninfct  12208  nn0seqcvgd  12209  eucalgf  12223  eucalginv  12224  lcmval  12231  prmind2  12288  dfphi2  12388  phiprmpw  12390  phimullem  12393  eulerthlem1  12395  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  eulerth  12401  phisum  12409  odzcllem  12411  odzdvds  12414  pythagtriplem19  12451  pclemub  12456  pcprecl  12458  pceu  12464  pcqmul  12472  pcqcl  12475  pcxnn0cl  12479  pcxqcl  12481  pcge0  12482  pcdvdsb  12489  pceq0  12491  pcneg  12494  pcdvdstr  12496  pcgcd1  12497  pc2dvds  12499  pcz  12501  pcprmpw2  12502  pcaddlem  12508  pcadd  12509  pcmptcl  12511  pcmpt  12512  pcmptdvds  12514  fldivp1  12517  qexpz  12521  pockthlem  12525  pockthg  12526  prmunb  12531  1arith  12536  4sqlemffi  12565  4sqlem17  12576  4sqlem18  12577  4sqlem19  12578  ennnfonelemom  12625  ennnfoneleminc  12628  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemdm  12637  ennnfonelemr  12640  ennnfonelemim  12641  exmidunben  12643  ctinfom  12645  inffinp1  12646  ctinf  12647  enctlem  12649  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  ctiunctlemudc  12654  ctiunct  12657  ctiunctal  12658  unct  12659  ssomct  12662  nninfdclemcl  12665  nninfdclemp1  12667  nninfdc  12670  structcnvcnv  12694  setscom  12718  relelbasov  12740  ressbas2d  12746  ressval3d  12750  ressabsg  12754  restid2  12919  imasaddfnlemg  12957  quslem  12967  ercpbl  12974  fnpr2ob  12983  mgmplusf  13009  grpinvalem  13028  grpinva  13029  grprida  13030  fngsum  13031  igsumvalx  13032  gsum0g  13039  gsumval2  13040  ismnd  13060  mhmpropd  13098  grppropd  13149  grpsubf  13211  dfgrp3mlem  13230  mulgnn0p1  13263  mulgnn0subcl  13265  mulgsubcl  13266  mulgneg  13270  mulgnn0dir  13282  mulgnn0ass  13288  submmulg  13296  issubg2m  13319  issubg4m  13323  ghmmulg  13386  ghmrn  13387  lringuplu  13752  lmodscaf  13866  lssintclm  13940  lspun0  13981  lidlbas  14034  topontopon  14256  eltg3i  14292  epttop  14326  difopn  14344  uncld  14349  0nnei  14389  resttopon  14407  restabs  14411  restopnb  14417  lmcvg  14453  cnptopco  14458  cnss1  14462  cnss2  14463  cncnpi  14464  cncnp2m  14467  cnrest  14471  cnrest2  14472  cnrest2r  14473  cnptoprest  14475  cnptoprest2  14476  lmss  14482  lmff  14485  lmtopcnp  14486  lmcn  14487  txbasval  14503  upxp  14508  txcnmpt  14509  txdis1cn  14514  txlm  14515  lmcn2  14516  cnmpt11  14519  cnmpt11f  14520  cnmpt1t  14521  cnmpt12  14523  cnmpt21  14527  cnmpt21f  14528  cnmpt2t  14529  cnmpt22  14530  cnmpt22f  14531  cnmptcom  14534  hmeocnv  14543  hmeof1o  14545  hmeores  14551  txhmeo  14555  txswaphmeo  14557  isxmet2d  14584  blfvalps  14621  xblss2ps  14640  xblss2  14641  blfps  14645  blf  14646  unirnblps  14658  unirnbl  14659  isxms2  14688  bdxmet  14737  bdmet  14738  xmetxp  14743  xmettx  14746  blssioo  14789  tgioo  14790  mulcncflem  14843  divcncfap  14850  dedekindeulemuub  14853  dedekindeulemub  14854  dedekindeulemloc  14855  dedekindeulemlu  14857  suplociccreex  14860  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemub  14863  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthdich  14889  limcrcl  14894  limcmpted  14899  limccnp2lem  14912  limccnp2cntop  14913  limccoap  14914  dvrecap  14949  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  plyco  14995  plycj  14997  plyrecj  14999  dvply1  15001  dvply2g  15002  cosordlem  15085  logbgcd1irraplemexp  15204  logbgcd1irrap  15206  lgsneg1  15266  lgsdilem  15268  lgsdir2  15274  lgsdirprm  15275  lgsdir  15276  lgsne0  15279  lgsabs1  15280  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1f1o  15301  gausslemma2dlem4  15305  lgseisenlem1  15311  lgsquadlem3  15320  2lgslem1a  15329  2sqlem5  15360  2sqlem7  15362  2sqlem8a  15363  2sqlem8  15364  2sqlem9  15365  bj-stand  15394  bj-charfundcALT  15455  bj-charfunbi  15457  bj-bdfindis  15593  bj-peano4  15601  strcollnfALT  15632  1dom1el  15637  pwtrufal  15642  pwf1oexmid  15644  subctctexmid  15645  pw1nct  15647  nnsf  15649  nninfalllem1  15652  nninfall  15653  nninfsellemqall  15659  nnnninfen  15665  exmidsbthrlem  15666  sbthom  15670  cvgcmp2nlemabs  15676  trilpo  15687  iswomni0  15695  redcwlpo  15699  dceqnconst  15704  dcapnconst  15705  nconstwlpolem  15709  nconstwlpo  15710  neapmkvlem  15711  neapmkv  15712  ltlenmkv  15714  taupi  15717  alsi1d  15725  alsi2d  15726  alsc1d  15727  alsc2d  15728