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  397  pm4.71rd  398  imdistand  451  orcomd  741  3mix3  1199  mpjao3dan  1348  ecase23d  1391  exlimdh  1649  nexd  1666  alexnim  1701  excomim  1715  19.41  1738  equcomd  1759  nfexd  1814  sbh  1829  sbcof2  1863  sbidm  1904  sb6rf  1906  nfsbt  2036  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eu2  2131  2euex  2174  eqcomd  2244  3eltr3g  2323  abbid  2355  neneqd  2441  eqnetrrid  2451  3netr3g  2454  necomd  2506  r19.21bi  2638  nrexdv  2643  rexlimd  2665  rabbidva  2809  elisset  2836  euind  3013  rmoan  3026  reuind  3031  2rmorex  3032  spsbc  3063  spesbc  3138  eldifad  3231  eldifbd  3232  3sstr3g  3290  sseqtrdi  3296  difindiss  3485  un00  3566  vvin  3568  undifss  3605  ifcldcd  3675  disjpr2  3769  difprsn1  3849  diftpsn3  3851  difsnss  3856  sneqr  3880  preqr1  3888  preq12b  3890  oprcl  3923  intab  3994  riinm  4080  rintm  4100  disjiun  4120  sndisj  4121  3brtr3g  4158  trint  4239  iinexgm  4285  exmidexmid  4328  exmid01  4330  pwntru  4331  exmid1stab  4340  pwel  4353  exss  4362  0nelop  4383  euotd  4390  opelopabsb  4397  pwunim  4426  issod  4459  frind  4492  suctr  4561  orduniss  4565  onelini  4570  oneluni  4571  eusv2i  4596  rexxfrd  4604  rabxfrd  4610  reuhypd  4612  iunpw  4621  sucexg  4640  ordsucim  4642  ordtriexmidlem  4661  ontriexmidim  4664  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  ordsucunielexmid  4673  orddif  4689  suc11g  4699  onintexmid  4715  reg3exmidlemwe  4721  tfisi  4729  peano1  4736  peano2  4737  finds2  4743  omsinds  4764  brrelex12  4808  brel  4822  ssrel  4858  ssrel2  4860  ssrelrel  4870  elrel  4872  xpsspw  4882  relop  4925  dmxpm  4997  opelresi  5069  mptimass  5134  ndmima  5159  poirr2  5175  xpmlem  5203  xpimasn  5231  iotass  5350  iotacl  5357  dffun5r  5384  funeu  5397  funeu2  5398  funfnd  5403  funopg  5406  funun  5417  fununfun  5419  funinsn  5425  funtp  5429  funcnvuni  5445  funcnvres2  5451  imadiflem  5455  imadif  5456  funimaexglem  5459  fneu2  5483  fnimaeq0  5500  fnmpt  5505  ffrn  5540  fun2  5557  f00  5579  f0bi  5580  fimadmfo  5619  foimacnv  5652  resdif  5656  f1ococnv1  5663  fv3  5713  relelfvdm  5722  elfvm  5723  nfvres  5726  dffn5im  5742  mptfvex  5785  fvmptdf  5787  fvmptdv2  5789  fndmdif  5805  dff4im  5845  fmpt  5849  fmptd  5853  fmptdf  5856  f1oresrab  5864  fcoconst  5870  fsn  5871  funopsn  5882  ftpg  5890  fsnunf  5906  resfunexg  5927  isores1  6010  riota2df  6050  acexmidlemcase  6070  brabvv  6124  funoprabg  6177  fnovim  6187  ovmpodf  6210  ovi3  6216  elmpocl  6274  uchoice  6361  1stcof  6387  2ndcof  6388  opabn1stprc  6419  fnmpo  6428  fmpoco  6442  fo2ndf  6453  f1o2ndf1  6454  disjxp1  6462  fvdifsuppst  6474  fsuppeq  6477  fsuppeqg  6478  suppssrst  6491  suppssrgst  6492  brtpos2  6512  reldmtpos  6514  dftpos3  6523  dftpos4  6524  tpostpos2  6526  tposf2  6529  tposf12  6530  tposfo  6532  tposf  6533  smores2  6555  tfrlem1  6569  tfrlem3-2d  6573  tfrlemisucaccv  6586  tfrlemibxssdm  6588  tfrlemibfn  6589  tfrlemi1  6593  tfrexlem  6595  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcldm  6624  rdgivallem  6642  rdgisucinc  6646  frecabex  6659  frecfnom  6662  frecfcllem  6665  frecsuclem  6667  omsuc  6735  nntri2  6757  nnsucuniel  6758  nnsseleq  6764  nnm00  6793  ecexr  6802  swoer  6825  elqsn0m  6867  iinerm  6871  erinxp  6873  ecinxp  6874  eroveu  6890  eroprf  6892  mapprc  6916  mapsn  6962  ixpprc  6991  ixp0  7003  resixp  7005  elixpsn  7007  dom2lem  7048  fundmen  7084  1dom1el  7097  dom0  7128  xpf1o  7134  mapxpen  7138  xpmapenlem  7139  ssenen  7142  nneneq  7148  ssfilem  7167  ssfilemd  7169  dif1en  7173  dif1enen  7174  fin0  7179  fin0or  7180  diffitest  7181  diffisn  7187  ac6sfi  7192  fimax2gtrilemstep  7195  fimax2gtri  7196  finexdc  7197  eqsndc  7200  exmidpweq  7206  pw1fin  7207  onunsnss  7214  unsnfidcel  7218  undifdcss  7220  undifdc  7221  tpfidceq  7227  fiintim  7228  fisseneq  7232  fidcenumlemr  7262  sbthlemi4  7267  sbthlemi5  7268  sbthlemi9  7272  fifo  7304  2omap  7308  suplubti  7330  supelti  7332  infmoti  7358  infisoti  7362  djulclb  7385  updjud  7412  omp1eomlem  7424  0ct  7437  ctmlemr  7438  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumct  7445  nninfninc  7453  nnnninfeq2  7459  finomni  7470  fodjuomnilemdc  7474  fodjum  7476  fodjuomnilemres  7478  fodjumkvlemres  7489  omniwomnimkv  7497  nninfwlporlem  7503  nninfwlpoimlemginf  7506  nninfwlpoim  7509  nninfinfwlpo  7510  ficardon  7524  pr2cv1  7531  exmidonfinlem  7535  en2eleq  7537  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  exmidfodomrlemim  7543  finacn  7550  acfun  7553  exmidaclem  7554  exmidontriimlem3  7569  exmidontriimlem4  7570  exmidontriim  7571  pw1if  7574  pw1on  7575  papsym  7602  papcotr  7603  dftap2  7607  2omotaplemst  7614  exmidapne  7616  ccfunen  7620  cc1  7621  cc2lem  7622  cc2  7623  cc3  7624  acnccim  7628  elni2  7671  indpi  7699  distrnqg  7744  subhalfnqq  7771  enq0sym  7789  enq0ref  7790  enq0tr  7791  nqnq0pi  7795  nnnq0lem1  7803  distrnq0  7816  elinp  7831  elnp1st2nd  7833  prltlu  7844  prnmaxl  7845  prnminu  7846  prarloc  7860  nqprm  7899  appdivnq  7920  prmuloc  7923  mullocpr  7928  distrlem4prl  7941  distrlem4pru  7942  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  cauappcvgprlemopl  8003  cauappcvgprlemopu  8005  cauappcvgprlemdisj  8008  cauappcvgprlem2  8017  cauappcvgprlemlim  8018  caucvgprlemnkj  8023  caucvgprlemopl  8026  caucvgprlemopu  8028  caucvgprlemdisj  8031  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem2  8037  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemlol  8055  caucvgprprlemexbt  8063  caucvgprprlem1  8066  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  suplocexprlemlub  8081  prsrlem1  8099  gt0srpr  8105  caucvgsrlemcl  8146  caucvgsrlembound  8151  caucvgsrlemgt1  8152  suplocsrlemb  8163  suplocsrlem  8165  suplocsr  8166  ltresr  8196  nnindnn  8250  axcaucvglemcl  8252  axcaucvglemval  8254  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  sup3exmid  9277  nnind  9299  nn0supp  9598  nn0ge2m1nn  9606  zleloe  9670  zapne  9698  nn0lt2  9706  suprzclex  9723  zindd  9743  uzm1  9932  uzin  9934  infregelbex  9977  elnn1uz2  9986  nn01to3  9996  divfnzn  10000  qapne  10018  xrltnsym2  10175  xaddass  10250  xleadd1a  10254  xlt2add  10261  xlesubadd  10264  iooval2  10296  icoshftf1o  10372  fztri3or  10422  fzneuz  10486  4fvwrd4  10525  elfzo0  10571  infssuzex  10644  infssuzcldc  10646  infssfzcldc  10647  infssfzledc  10648  suprzubdc  10649  nninfdcex  10650  zsupssdc  10651  exbtwnzlemex  10662  ioom  10673  fzfig  10845  uzennn  10851  uzsinds  10859  iseqovex  10873  seq3val  10875  seqvalcd  10876  seqf  10879  seqovcd  10882  monoord2  10901  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  seq3f1olemqsum  10928  seq3f1o  10932  seqf1og  10936  seq3distr  10947  expp1  10961  expcl2lemap  10966  expclzap  10979  expap0i  10986  nn0ltexp2  11125  bcval5  11179  hashinfuni  11194  hashennnuni  11196  hashnncl  11212  resunimafz0  11252  hashf1lem2  11264  hashf1  11265  zfz1isolemiso  11269  zfz1isolem1  11270  zfz1iso  11271  wrdsymb0  11315  wrdlen1  11320  ccat1st1st  11387  swrdrlen  11411  pfxid  11436  pfxwrdsymbg  11440  pfxtrcfv  11443  pfxccat1  11452  pfxpfxid  11459  pfxcctswrd  11460  swrdccatin1  11475  pfxccatin12  11483  pfxccatid  11491  seq3shft  11581  cvg1nlemcau  11728  rexanuz  11732  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  rersqreu  11772  caubnd2  11861  maxleast  11957  fimaxre2  11971  minmax  11974  xrmaxiflemcl  11989  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxadd  12005  xrminmax  12009  xrbdtri  12020  climreu  12041  reccn2ap  12057  iserex  12083  climcvg1nlem  12093  serf0  12096  fz1f1o  12119  summodclem3  12125  zsumdc  12129  fsum3  12132  isumz  12134  isumss  12136  isumss2  12138  fsumsersdc  12140  fsum3ser  12142  fsumsplit  12152  isumclim2  12167  isumclim3  12168  fsum2dlemstep  12179  fsumcnv  12182  fisumcom2  12183  bcxmas  12234  isumle  12240  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratz  12277  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  zproddc  12324  prod1dc  12331  fprodsplitdc  12341  fprodsplit  12342  fprodunsn  12349  fprodcl2lem  12350  fprodcllemf  12358  fprod2dlemstep  12367  fprodcnv  12370  fprodcom2fi  12371  fprodle  12385  ef0lem  12405  fsumdvds  12587  mod2eq1n2dvds  12624  ndvdssub  12675  bitsfzolem  12699  bitsfzo  12700  bitsinv1  12707  gcdsupex  12712  gcdsupcl  12713  bezoutlemnewy  12751  bezoutlemmain  12753  bezoutlembi  12760  bezoutlemeu  12762  bezoutlemle  12763  uzwodc  12792  nnwofdc  12793  nnwosdc  12794  nninfctlemfo  12795  nninfct  12796  nn0seqcvgd  12797  eucalgf  12811  eucalginv  12812  lcmval  12819  prmind2  12876  dfphi2  12976  phiprmpw  12978  phimullem  12981  eulerthlem1  12983  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  eulerth  12989  phisum  12997  odzcllem  12999  odzdvds  13002  pythagtriplem19  13039  pclemub  13044  pcprecl  13046  pceu  13052  pcqmul  13060  pcqcl  13063  pcxnn0cl  13067  pcxqcl  13069  pcge0  13070  pcdvdsb  13077  pceq0  13079  pcneg  13082  pcdvdstr  13084  pcgcd1  13085  pc2dvds  13087  pcz  13089  pcprmpw2  13090  pcaddlem  13096  pcadd  13097  pcmptcl  13099  pcmpt  13100  pcmptdvds  13102  fldivp1  13105  qexpz  13109  pockthlem  13113  pockthg  13114  prmunb  13119  1arith  13124  4sqlemffi  13153  4sqlem17  13164  4sqlem18  13165  4sqlem19  13166  ballotfilemcdc  13201  ballotfilem2  13206  ballotfilemfp1  13209  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfmpn  13212  ballotfilemefi  13215  ballotfilemiex  13222  ballotfilemro  13244  ennnfonelemom  13277  ennnfoneleminc  13280  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemdm  13289  ennnfonelemr  13292  ennnfonelemim  13293  exmidunben  13295  ctinfom  13297  inffinp1  13298  ctinf  13299  enctlem  13301  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  ctiunctlemudc  13306  ctiunct  13309  ctiunctal  13310  unct  13311  ssomct  13314  nninfdclemcl  13317  nninfdclemp1  13319  nninfdc  13322  structcnvcnv  13346  setscom  13370  relelbasov  13393  ressbas2d  13399  ressval3d  13403  ressabsg  13407  restid2  13579  imasaddfnlemg  13612  quslem  13622  ercpbl  13629  fnpr2ob  13638  mgmplusf  13663  grpinvalem  13682  grpinva  13683  grprida  13684  fngzsum  13685  gzsumvalx  13686  gzsum0  13690  gzsumval2  13691  ismnd  13709  mhmpropd  13750  grppropd  13799  grpsubf  13861  dfgrp3mlem  13880  mulgnn0p1  13913  mulgnn0subcl  13915  mulgsubcl  13916  mulgneg  13920  mulgnn0dir  13932  mulgnn0ass  13938  submmulg  13946  issubg2m  13969  issubg4m  13973  ghmmulg  14036  ghmrn  14037  gsumvalfi  14129  gzsumgsum  14132  gsumf1ofi  14137  gsummhmfi  14141  gsumressfi  14144  lringuplu  14476  rrgsupp  14547  opprdrng  14593  lmodscaf  14619  lssintclm  14693  lspun0  14734  lidlbas  14787  psrbagconcl  14986  psr1clfi  15002  topontopon  15044  eltg3i  15080  epttop  15114  difopn  15132  uncld  15137  0nnei  15177  resttopon  15195  restabs  15199  restopnb  15205  lmcvg  15241  cnptopco  15246  cnss1  15250  cnss2  15251  cncnpi  15252  cncnp2m  15255  cnrest  15259  cnrest2  15260  cnrest2r  15261  cnptoprest  15263  cnptoprest2  15264  lmss  15270  lmff  15273  lmtopcnp  15274  lmcn  15275  txbasval  15291  upxp  15296  txcnmpt  15297  txdis1cn  15302  txlm  15303  lmcn2  15304  cnmpt11  15307  cnmpt11f  15308  cnmpt1t  15309  cnmpt12  15311  cnmpt21  15315  cnmpt21f  15316  cnmpt2t  15317  cnmpt22  15318  cnmpt22f  15319  cnmptcom  15322  hmeocnv  15331  hmeof1o  15333  hmeores  15339  txhmeo  15343  txswaphmeo  15345  isxmet2d  15372  blfvalps  15409  xblss2ps  15428  xblss2  15429  blfps  15433  blf  15434  unirnblps  15446  unirnbl  15447  isxms2  15476  bdxmet  15525  bdmet  15526  xmetxp  15531  xmettx  15534  blssioo  15577  tgioo  15578  mulcncflem  15631  divcncfap  15638  dedekindeulemuub  15641  dedekindeulemub  15642  dedekindeulemloc  15643  dedekindeulemlu  15645  suplociccreex  15648  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemub  15651  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthdich  15677  limcrcl  15682  limcmpted  15687  limccnp2lem  15700  limccnp2cntop  15701  limccoap  15702  dvrecap  15737  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plyco  15783  plycj  15785  plyrecj  15787  dvply1  15789  dvply2g  15790  cosordlem  15873  logbgcd1irraplemexp  15993  logbgcd1irrap  15995  lgsneg1  16058  lgsdilem  16060  lgsdir2  16066  lgsdirprm  16067  lgsdir  16068  lgsne0  16071  lgsabs1  16072  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1f1o  16093  gausslemma2dlem4  16097  lgseisenlem1  16103  lgsquadlem3  16112  2lgslem1a  16121  2sqlem5  16152  2sqlem7  16154  2sqlem8a  16155  2sqlem8  16156  2sqlem9  16157  gropeld  16204  grstructeld2dom  16205  uhgrm  16233  upgrm  16255  upgr1een  16279  uhgredgm  16291  edgupgren  16296  edgumgren  16297  edgusgren  16318  ausgrusgrben  16323  umgr2edg1  16364  usgredg2vlem1  16377  uhgr0enedgfi  16391  subupgr  16428  vtxedgfi  16444  vtxlpfi  16445  vtxdumgrfival  16453  vtxd0nedgbfi  16454  1hevtxdg0fi  16462  p1evtxdeqfilem  16466  wlkvtxm  16495  g0wlk0  16525  wlkres  16534  trlreslem  16544  clwwlkccatlem  16555  clwwlknnn  16567  trlsegvdeglem6  16620  eupth2lem3lem3fi  16625  eupth2lem3lem7fi  16629  eulerpathum  16636  dichmul0or  16674  bj-stand  16690  bj-charfundcALT  16749  bj-charfunbi  16751  bj-bdfindis  16887  bj-peano4  16895  strcollnfALT  16926  pw1map  16939  pwtrufal  16941  pwf1oexmid  16943  subctctexmid  16944  pw1nct  16947  nnsf  16953  nninfalllem1  16956  nninfall  16957  nninfsellemqall  16963  nnnninfen  16969  exmidsbthrlem  16972  sbthom  16976  repiecef  16982  cvgcmp2nlemabs  16986  trilpo  16997  iswomni0  17006  redcwlpo  17010  dceqnconst  17015  dcapnconst  17016  nconstwlpolem  17020  nconstwlpo  17021  neapmkvlem  17022  neapmkv  17023  ltlenmkv  17025  taupi  17028  alsi1d  17036  alsi2d  17037  alsc1d  17038  alsc2d  17039