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  734  3mix3  1192  mpjao3dan  1341  ecase23d  1384  exlimdh  1642  nexd  1659  alexnim  1694  excomim  1709  19.41  1732  equcomd  1753  nfexd  1807  sbh  1822  sbcof2  1856  sbidm  1897  sb6rf  1899  nfsbt  2027  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eu2  2122  2euex  2165  eqcomd  2235  3eltr3g  2314  abbid  2346  neneqd  2421  eqnetrrid  2431  3netr3g  2434  necomd  2486  r19.21bi  2618  nrexdv  2623  rexlimd  2645  rabbidva  2787  elisset  2814  euind  2990  rmoan  3003  reuind  3008  2rmorex  3009  spsbc  3040  spesbc  3115  eldifad  3208  eldifbd  3209  3sstr3g  3266  sseqtrdi  3272  difindiss  3458  un00  3538  undifss  3572  ifcldcd  3640  disjpr2  3730  difprsn1  3806  diftpsn3  3808  difsnss  3813  sneqr  3837  preqr1  3845  preq12b  3847  oprcl  3880  intab  3951  riinm  4037  rintm  4057  disjiun  4077  sndisj  4078  3brtr3g  4115  trint  4196  iinexgm  4237  exmidexmid  4279  exmid01  4281  pwntru  4282  exmid1stab  4291  pwel  4303  exss  4312  0nelop  4333  euotd  4340  opelopabsb  4347  pwunim  4374  issod  4407  frind  4440  suctr  4509  orduniss  4513  onelini  4518  oneluni  4519  eusv2i  4543  rexxfrd  4551  rabxfrd  4557  reuhypd  4559  iunpw  4568  sucexg  4587  ordsucim  4589  ordtriexmidlem  4608  ontriexmidim  4611  ordtri2or2exmidlem  4615  onsucelsucexmidlem  4618  ordsucunielexmid  4620  orddif  4636  suc11g  4646  onintexmid  4662  reg3exmidlemwe  4668  tfisi  4676  peano1  4683  peano2  4684  finds2  4690  omsinds  4711  brrelex12  4754  brel  4768  ssrel  4804  ssrel2  4806  ssrelrel  4816  elrel  4818  xpsspw  4828  relop  4869  dmxpm  4940  opelresi  5012  mptimass  5077  ndmima  5101  poirr2  5117  xpmlem  5145  xpimasn  5173  iotass  5292  iotacl  5299  dffun5r  5326  funeu  5339  funeu2  5340  funfnd  5345  funopg  5348  funun  5358  fununfun  5360  funinsn  5366  funtp  5370  funcnvuni  5386  funcnvres2  5392  imadiflem  5396  imadif  5397  funimaexglem  5400  fneu2  5424  fnimaeq0  5441  fnmpt  5446  fun2  5494  f00  5513  f0bi  5514  fimadmfo  5553  foimacnv  5586  resdif  5590  f1ococnv1  5597  fv3  5646  relelfvdm  5655  elfvm  5656  nfvres  5657  dffn5im  5672  mptfvex  5713  fvmptdf  5715  fvmptdv2  5717  fndmdif  5733  dff4im  5774  fmpt  5778  fmptd  5782  fmptdf  5785  f1oresrab  5793  fcoconst  5799  fsn  5800  funopsn  5810  ftpg  5816  fsnunf  5832  resfunexg  5853  isores1  5931  riota2df  5969  acexmidlemcase  5989  brabvv  6041  funoprabg  6094  fnovim  6104  ovmpodf  6127  ovi3  6133  elmpocl  6191  uchoice  6273  1stcof  6299  2ndcof  6300  fnmpo  6338  fmpoco  6352  fo2ndf  6363  f1o2ndf1  6364  disjxp1  6372  brtpos2  6387  reldmtpos  6389  dftpos3  6398  dftpos4  6399  tpostpos2  6401  tposf2  6404  tposf12  6405  tposfo  6407  tposf  6408  smores2  6430  tfrlem1  6444  tfrlem3-2d  6448  tfrlemisucaccv  6461  tfrlemibxssdm  6463  tfrlemibfn  6464  tfrlemi1  6468  tfrexlem  6470  tfr1onlemsucaccv  6477  tfr1onlembxssdm  6479  tfr1onlembfn  6480  tfr1onlemaccex  6484  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllembfn  6493  tfrcllemaccex  6497  tfrcldm  6499  rdgivallem  6517  rdgisucinc  6521  frecabex  6534  frecfnom  6537  frecfcllem  6540  frecsuclem  6542  omsuc  6608  nntri2  6630  nnsucuniel  6631  nnsseleq  6637  nnm00  6666  ecexr  6675  swoer  6698  elqsn0m  6740  iinerm  6744  erinxp  6746  ecinxp  6747  eroveu  6763  eroprf  6765  mapprc  6789  mapsn  6827  ixpprc  6856  ixp0  6868  resixp  6870  elixpsn  6872  dom2lem  6913  fundmen  6949  dom0  6987  xpf1o  6993  mapxpen  6997  xpmapenlem  6998  ssenen  7000  nneneq  7006  ssfilem  7025  dif1en  7029  dif1enen  7030  fin0  7035  fin0or  7036  diffitest  7037  diffisn  7043  ac6sfi  7048  fimax2gtrilemstep  7050  fimax2gtri  7051  finexdc  7052  exmidpweq  7059  pw1fin  7060  onunsnss  7067  unsnfidcel  7071  undifdcss  7073  undifdc  7074  tpfidceq  7080  fiintim  7081  fisseneq  7084  fidcenumlemr  7110  sbthlemi4  7115  sbthlemi5  7116  sbthlemi9  7120  fifo  7135  suplubti  7155  supelti  7157  infmoti  7183  infisoti  7187  djulclb  7210  updjud  7237  omp1eomlem  7249  0ct  7262  ctmlemr  7263  ctssdclemn0  7265  ctssdccl  7266  ctssdc  7268  enumct  7270  nninfninc  7278  nnnninfeq2  7284  finomni  7295  fodjuomnilemdc  7299  fodjum  7301  fodjuomnilemres  7303  fodjumkvlemres  7314  omniwomnimkv  7322  nninfwlporlem  7328  nninfwlpoimlemginf  7331  nninfwlpoim  7334  nninfinfwlpo  7335  ficardon  7349  pr2cv1  7356  exmidonfinlem  7359  en2eleq  7361  exmidfodomrlemeldju  7365  exmidfodomrlemreseldju  7366  exmidfodomrlemim  7367  finacn  7374  acfun  7377  exmidaclem  7378  exmidontriimlem3  7393  exmidontriimlem4  7394  exmidontriim  7395  pw1if  7398  pw1on  7399  dftap2  7425  2omotaplemst  7432  exmidapne  7434  ccfunen  7438  cc1  7439  cc2lem  7440  cc2  7441  cc3  7442  acnccim  7446  elni2  7489  indpi  7517  distrnqg  7562  subhalfnqq  7589  enq0sym  7607  enq0ref  7608  enq0tr  7609  nqnq0pi  7613  nnnq0lem1  7621  distrnq0  7634  elinp  7649  elnp1st2nd  7651  prltlu  7662  prnmaxl  7663  prnminu  7664  prarloc  7678  nqprm  7717  appdivnq  7738  prmuloc  7741  mullocpr  7746  distrlem4prl  7759  distrlem4pru  7760  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemopu  7778  cauappcvgprlemopl  7821  cauappcvgprlemopu  7823  cauappcvgprlemdisj  7826  cauappcvgprlem2  7835  cauappcvgprlemlim  7836  caucvgprlemnkj  7841  caucvgprlemopl  7844  caucvgprlemopu  7846  caucvgprlemdisj  7849  caucvgprlemcl  7851  caucvgprlemladdfu  7852  caucvgprlemladdrl  7853  caucvgprlem2  7855  caucvgprprlemcbv  7862  caucvgprprlemval  7863  caucvgprprlemlol  7873  caucvgprprlemexbt  7881  caucvgprprlem1  7884  suplocexprlemrl  7892  suplocexprlemmu  7893  suplocexprlemru  7894  suplocexprlemdisj  7895  suplocexprlemloc  7896  suplocexprlemub  7898  suplocexprlemlub  7899  prsrlem1  7917  gt0srpr  7923  caucvgsrlemcl  7964  caucvgsrlembound  7969  caucvgsrlemgt1  7970  suplocsrlemb  7981  suplocsrlem  7983  suplocsr  7984  ltresr  8014  nnindnn  8068  axcaucvglemcl  8070  axcaucvglemval  8072  axcaucvglemcau  8073  axcaucvglemres  8074  axpre-suploclemres  8076  axpre-suploc  8077  sup3exmid  9092  nnind  9114  nn0supp  9409  nn0ge2m1nn  9417  zleloe  9481  zapne  9509  nn0lt2  9516  suprzclex  9533  zindd  9553  uzm1  9741  uzin  9743  infregelbex  9781  elnn1uz2  9790  nn01to3  9800  divfnzn  9804  qapne  9822  xrltnsym2  9978  xaddass  10053  xleadd1a  10057  xlt2add  10064  xlesubadd  10067  iooval2  10099  icoshftf1o  10175  fztri3or  10223  fzneuz  10285  4fvwrd4  10324  elfzo0  10370  infssuzex  10440  infssuzcldc  10442  suprzubdc  10443  nninfdcex  10444  zsupssdc  10445  exbtwnzlemex  10456  ioom  10467  fzfig  10639  uzennn  10645  uzsinds  10653  iseqovex  10667  seq3val  10669  seqvalcd  10670  seqf  10673  seqovcd  10676  monoord2  10695  iseqf1olemjpcl  10717  iseqf1olemqpcl  10718  seq3f1olemqsum  10722  seq3f1o  10726  seqf1og  10730  seq3distr  10741  expp1  10755  expcl2lemap  10760  expclzap  10773  expap0i  10780  nn0ltexp2  10918  bcval5  10972  hashinfuni  10986  hashennnuni  10988  hashnncl  11004  resunimafz0  11040  zfz1isolemiso  11048  zfz1isolem1  11049  zfz1iso  11050  wrdsymb0  11090  wrdlen1  11095  ccat1st1st  11158  swrdrlen  11179  pfxid  11204  pfxwrdsymbg  11208  pfxtrcfv  11211  pfxccat1  11220  pfxpfxid  11227  pfxcctswrd  11228  swrdccatin1  11243  pfxccatin12  11251  pfxccatid  11259  seq3shft  11335  cvg1nlemcau  11481  rexanuz  11485  resqrexlemoverl  11518  resqrexlemglsq  11519  resqrexlemsqa  11521  resqrexlemex  11522  rersqreu  11525  caubnd2  11614  maxleast  11710  fimaxre2  11724  minmax  11727  xrmaxiflemcl  11742  xrmaxiflemab  11744  xrmaxiflemlub  11745  xrmaxadd  11758  xrminmax  11762  xrbdtri  11773  climreu  11794  reccn2ap  11810  iserex  11836  climcvg1nlem  11846  serf0  11849  fz1f1o  11872  summodclem3  11877  zsumdc  11881  fsum3  11884  isumz  11886  isumss  11888  isumss2  11890  fsumsersdc  11892  fsum3ser  11894  fsumsplit  11904  isumclim2  11919  isumclim3  11920  fsum2dlemstep  11931  fsumcnv  11934  fisumcom2  11935  bcxmas  11986  isumle  11992  cvgratnnlemnexp  12021  cvgratnnlemmn  12022  cvgratz  12029  mertenslemub  12031  mertenslemi1  12032  mertenslem2  12033  mertensabs  12034  zproddc  12076  prod1dc  12083  fprodsplitdc  12093  fprodsplit  12094  fprodunsn  12101  fprodcl2lem  12102  fprodcllemf  12110  fprod2dlemstep  12119  fprodcnv  12122  fprodcom2fi  12123  fprodle  12137  ef0lem  12157  fsumdvds  12339  mod2eq1n2dvds  12376  ndvdssub  12427  bitsfzolem  12451  bitsfzo  12452  bitsinv1  12459  gcdsupex  12464  gcdsupcl  12465  bezoutlemnewy  12503  bezoutlemmain  12505  bezoutlembi  12512  bezoutlemeu  12514  bezoutlemle  12515  uzwodc  12544  nnwofdc  12545  nnwosdc  12546  nninfctlemfo  12547  nninfct  12548  nn0seqcvgd  12549  eucalgf  12563  eucalginv  12564  lcmval  12571  prmind2  12628  dfphi2  12728  phiprmpw  12730  phimullem  12733  eulerthlem1  12735  eulerthlemrprm  12737  eulerthlema  12738  eulerthlemh  12739  eulerthlemth  12740  eulerth  12741  phisum  12749  odzcllem  12751  odzdvds  12754  pythagtriplem19  12791  pclemub  12796  pcprecl  12798  pceu  12804  pcqmul  12812  pcqcl  12815  pcxnn0cl  12819  pcxqcl  12821  pcge0  12822  pcdvdsb  12829  pceq0  12831  pcneg  12834  pcdvdstr  12836  pcgcd1  12837  pc2dvds  12839  pcz  12841  pcprmpw2  12842  pcaddlem  12848  pcadd  12849  pcmptcl  12851  pcmpt  12852  pcmptdvds  12854  fldivp1  12857  qexpz  12861  pockthlem  12865  pockthg  12866  prmunb  12871  1arith  12876  4sqlemffi  12905  4sqlem17  12916  4sqlem18  12917  4sqlem19  12918  ennnfonelemom  12965  ennnfoneleminc  12968  ennnfonelemhf1o  12970  ennnfonelemex  12971  ennnfonelemhom  12972  ennnfonelemdm  12977  ennnfonelemr  12980  ennnfonelemim  12981  exmidunben  12983  ctinfom  12985  inffinp1  12986  ctinf  12987  enctlem  12989  ctiunctlemu1st  12991  ctiunctlemu2nd  12992  ctiunctlemudc  12994  ctiunct  12997  ctiunctal  12998  unct  12999  ssomct  13002  nninfdclemcl  13005  nninfdclemp1  13007  nninfdc  13010  structcnvcnv  13034  setscom  13058  relelbasov  13081  ressbas2d  13087  ressval3d  13091  ressabsg  13095  restid2  13267  imasaddfnlemg  13333  quslem  13343  ercpbl  13350  fnpr2ob  13359  mgmplusf  13385  grpinvalem  13404  grpinva  13405  grprida  13406  fngsum  13407  igsumvalx  13408  gsum0g  13415  gsumval2  13416  ismnd  13438  mhmpropd  13485  grppropd  13536  grpsubf  13598  dfgrp3mlem  13617  mulgnn0p1  13656  mulgnn0subcl  13658  mulgsubcl  13659  mulgneg  13663  mulgnn0dir  13675  mulgnn0ass  13681  submmulg  13689  issubg2m  13712  issubg4m  13716  ghmmulg  13779  ghmrn  13780  lringuplu  14145  lmodscaf  14259  lssintclm  14333  lspun0  14374  lidlbas  14427  psr1clfi  14637  topontopon  14679  eltg3i  14715  epttop  14749  difopn  14767  uncld  14772  0nnei  14812  resttopon  14830  restabs  14834  restopnb  14840  lmcvg  14876  cnptopco  14881  cnss1  14885  cnss2  14886  cncnpi  14887  cncnp2m  14890  cnrest  14894  cnrest2  14895  cnrest2r  14896  cnptoprest  14898  cnptoprest2  14899  lmss  14905  lmff  14908  lmtopcnp  14909  lmcn  14910  txbasval  14926  upxp  14931  txcnmpt  14932  txdis1cn  14937  txlm  14938  lmcn2  14939  cnmpt11  14942  cnmpt11f  14943  cnmpt1t  14944  cnmpt12  14946  cnmpt21  14950  cnmpt21f  14951  cnmpt2t  14952  cnmpt22  14953  cnmpt22f  14954  cnmptcom  14957  hmeocnv  14966  hmeof1o  14968  hmeores  14974  txhmeo  14978  txswaphmeo  14980  isxmet2d  15007  blfvalps  15044  xblss2ps  15063  xblss2  15064  blfps  15068  blf  15069  unirnblps  15081  unirnbl  15082  isxms2  15111  bdxmet  15160  bdmet  15161  xmetxp  15166  xmettx  15169  blssioo  15212  tgioo  15213  mulcncflem  15266  divcncfap  15273  dedekindeulemuub  15276  dedekindeulemub  15277  dedekindeulemloc  15278  dedekindeulemlu  15280  suplociccreex  15283  suplociccex  15284  dedekindicclemuub  15285  dedekindicclemub  15286  dedekindicclemloc  15287  dedekindicclemlu  15289  dedekindicc  15292  ivthinclemlopn  15295  ivthinclemuopn  15297  ivthdich  15312  limcrcl  15317  limcmpted  15322  limccnp2lem  15335  limccnp2cntop  15336  limccoap  15337  dvrecap  15372  plyaddlem1  15406  plymullem1  15407  plycoeid3  15416  plyco  15418  plycj  15420  plyrecj  15422  dvply1  15424  dvply2g  15425  cosordlem  15508  logbgcd1irraplemexp  15627  logbgcd1irrap  15629  lgsneg1  15689  lgsdilem  15691  lgsdir2  15697  lgsdirprm  15698  lgsdir  15699  lgsne0  15702  lgsabs1  15703  lgsdirnn0  15711  lgsdinn0  15712  gausslemma2dlem1f1o  15724  gausslemma2dlem4  15728  lgseisenlem1  15734  lgsquadlem3  15743  2lgslem1a  15752  2sqlem5  15783  2sqlem7  15785  2sqlem8a  15786  2sqlem8  15787  2sqlem9  15788  gropeld  15835  grstructeld2dom  15836  uhgrm  15863  upgrm  15885  uhgredgm  15919  edgupgren  15924  edgumgren  15925  edgusgren  15946  ausgrusgrben  15951  umgr2edg1  15992  usgredg2vlem1  16005  bj-stand  16042  bj-charfundcALT  16102  bj-charfunbi  16104  bj-bdfindis  16240  bj-peano4  16248  strcollnfALT  16279  1dom1el  16284  2omap  16290  pw1map  16292  pwtrufal  16294  pwf1oexmid  16296  subctctexmid  16297  pw1nct  16300  nnsf  16302  nninfalllem1  16305  nninfall  16306  nninfsellemqall  16312  nnnninfen  16318  exmidsbthrlem  16321  sbthom  16325  cvgcmp2nlemabs  16331  trilpo  16342  iswomni0  16350  redcwlpo  16354  dceqnconst  16359  dcapnconst  16360  nconstwlpolem  16364  nconstwlpo  16365  neapmkvlem  16366  neapmkv  16367  ltlenmkv  16369  taupi  16372  alsi1d  16380  alsi2d  16381  alsc1d  16382  alsc2d  16383