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  729  3mix3  1168  mpjao3dan  1307  ecase23d  1350  exlimdh  1596  nexd  1613  alexnim  1648  excomim  1663  19.41  1686  equcomd  1707  nfexd  1761  sbh  1776  sbcof2  1810  sbidm  1851  sb6rf  1853  nfsbt  1976  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eu2  2070  2euex  2113  eqcomd  2183  3eltr3g  2262  abbid  2294  neneqd  2368  eqnetrrid  2378  3netr3g  2381  necomd  2433  r19.21bi  2565  nrexdv  2570  rexlimd  2591  rabbidva  2726  elisset  2752  euind  2925  rmoan  2938  reuind  2943  2rmorex  2944  spsbc  2975  spesbc  3049  eldifad  3141  eldifbd  3142  3sstr3g  3198  sseqtrdi  3204  difindiss  3390  un00  3470  undifss  3504  ifcldcd  3571  disjpr2  3657  difprsn1  3732  diftpsn3  3734  difsnss  3739  sneqr  3761  preqr1  3769  preq12b  3771  oprcl  3803  intab  3874  riinm  3960  rintm  3980  disjiun  3999  sndisj  4000  3brtr3g  4037  trint  4117  iinexgm  4155  exmidexmid  4197  exmid01  4199  pwntru  4200  exmid1stab  4209  pwel  4219  exss  4228  0nelop  4249  euotd  4255  opelopabsb  4261  pwunim  4287  issod  4320  frind  4353  suctr  4422  orduniss  4426  onelini  4431  oneluni  4432  eusv2i  4456  rexxfrd  4464  rabxfrd  4470  reuhypd  4472  iunpw  4481  sucexg  4498  ordsucim  4500  ordtriexmidlem  4519  ontriexmidim  4522  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  ordsucunielexmid  4531  orddif  4547  suc11g  4557  onintexmid  4573  reg3exmidlemwe  4579  tfisi  4587  peano1  4594  peano2  4595  finds2  4601  omsinds  4622  brrelex12  4665  brel  4679  ssrel  4715  ssrel2  4717  ssrelrel  4727  elrel  4729  xpsspw  4739  relop  4778  dmxpm  4848  opelresi  4919  ndmima  5006  poirr2  5022  xpmlem  5050  xpimasn  5078  iotass  5196  iotacl  5202  dffun5r  5229  funeu  5242  funeu2  5243  funfnd  5248  funopg  5251  funun  5261  funinsn  5266  funtp  5270  funcnvuni  5286  funcnvres2  5292  imadiflem  5296  imadif  5297  funimaexglem  5300  fneu2  5322  fnimaeq0  5338  fnmpt  5343  fun2  5390  f00  5408  f0bi  5409  foimacnv  5480  resdif  5484  f1ococnv1  5491  fv3  5539  relelfvdm  5548  nfvres  5549  dffn5im  5562  mptfvex  5602  fvmptdf  5604  fvmptdv2  5606  fndmdif  5622  dff4im  5663  fmpt  5667  fmptd  5671  fmptdf  5674  f1oresrab  5682  fcoconst  5688  fsn  5689  ftpg  5701  fsnunf  5717  resfunexg  5738  isores1  5815  riota2df  5851  acexmidlemcase  5870  brabvv  5921  funoprabg  5974  fnovim  5983  ovmpodf  6006  ovi3  6011  elmpocl  6069  1stcof  6164  2ndcof  6165  fnmpo  6203  fmpoco  6217  fo2ndf  6228  f1o2ndf1  6229  disjxp1  6237  brtpos2  6252  reldmtpos  6254  dftpos3  6263  dftpos4  6264  tpostpos2  6266  tposf2  6269  tposf12  6270  tposfo  6272  tposf  6273  smores2  6295  tfrlem1  6309  tfrlem3-2d  6313  tfrlemisucaccv  6326  tfrlemibxssdm  6328  tfrlemibfn  6329  tfrlemi1  6333  tfrexlem  6335  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemaccex  6362  tfrcldm  6364  rdgivallem  6382  rdgisucinc  6386  frecabex  6399  frecfnom  6402  frecfcllem  6405  frecsuclem  6407  omsuc  6473  nntri2  6495  nnsucuniel  6496  nnsseleq  6502  nnm00  6531  ecexr  6540  swoer  6563  elqsn0m  6603  iinerm  6607  erinxp  6609  ecinxp  6610  eroveu  6626  eroprf  6628  mapprc  6652  mapsn  6690  ixpprc  6719  ixp0  6731  resixp  6733  elixpsn  6735  dom2lem  6772  fundmen  6806  dom0  6838  xpf1o  6844  mapxpen  6848  xpmapenlem  6849  ssenen  6851  nneneq  6857  ssfilem  6875  dif1en  6879  dif1enen  6880  fin0  6885  fin0or  6886  diffitest  6887  diffisn  6893  ac6sfi  6898  fimax2gtrilemstep  6900  fimax2gtri  6901  finexdc  6902  exmidpweq  6909  pw1fin  6910  onunsnss  6916  unsnfidcel  6920  undifdcss  6922  undifdc  6923  fiintim  6928  fisseneq  6931  fidcenumlemr  6954  sbthlemi4  6959  sbthlemi5  6960  sbthlemi9  6964  fifo  6979  suplubti  6999  supelti  7001  infmoti  7027  infisoti  7031  djulclb  7054  updjud  7081  omp1eomlem  7093  0ct  7106  ctmlemr  7107  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumct  7114  nnnninfeq2  7127  finomni  7138  fodjuomnilemdc  7142  fodjum  7144  fodjuomnilemres  7146  fodjumkvlemres  7157  omniwomnimkv  7165  nninfwlporlem  7171  nninfwlpoimlemginf  7174  nninfwlpoim  7176  exmidonfinlem  7192  en2eleq  7194  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  exmidfodomrlemim  7200  acfun  7206  exmidaclem  7207  exmidontriimlem3  7222  exmidontriimlem4  7223  exmidontriim  7224  pw1on  7225  dftap2  7250  2omotaplemst  7257  exmidapne  7259  ccfunen  7263  cc1  7264  cc2lem  7265  cc2  7266  cc3  7267  elni2  7313  indpi  7341  distrnqg  7386  subhalfnqq  7413  enq0sym  7431  enq0ref  7432  enq0tr  7433  nqnq0pi  7437  nnnq0lem1  7445  distrnq0  7458  elinp  7473  elnp1st2nd  7475  prltlu  7486  prnmaxl  7487  prnminu  7488  prarloc  7502  nqprm  7541  appdivnq  7562  prmuloc  7565  mullocpr  7570  distrlem4prl  7583  distrlem4pru  7584  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  cauappcvgprlemopl  7645  cauappcvgprlemopu  7647  cauappcvgprlemdisj  7650  cauappcvgprlem2  7659  cauappcvgprlemlim  7660  caucvgprlemnkj  7665  caucvgprlemopl  7668  caucvgprlemopu  7670  caucvgprlemdisj  7673  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem2  7679  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemlol  7697  caucvgprprlemexbt  7705  caucvgprprlem1  7708  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  prsrlem1  7741  gt0srpr  7747  caucvgsrlemcl  7788  caucvgsrlembound  7793  caucvgsrlemgt1  7794  suplocsrlemb  7805  suplocsrlem  7807  suplocsr  7808  ltresr  7838  nnindnn  7892  axcaucvglemcl  7894  axcaucvglemval  7896  axcaucvglemcau  7897  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  sup3exmid  8914  nnind  8935  nn0supp  9228  nn0ge2m1nn  9236  zleloe  9300  zapne  9327  nn0lt2  9334  suprzclex  9351  zindd  9371  uzm1  9558  uzin  9560  infregelbex  9598  elnn1uz2  9607  nn01to3  9617  divfnzn  9621  qapne  9639  xrltnsym2  9794  xaddass  9869  xleadd1a  9873  xlt2add  9880  xlesubadd  9883  iooval2  9915  icoshftf1o  9991  fztri3or  10039  fzneuz  10101  4fvwrd4  10140  elfzo0  10182  exbtwnzlemex  10250  ioom  10261  fzfig  10430  uzennn  10436  uzsinds  10442  iseqovex  10456  seq3val  10458  seqvalcd  10459  seqf  10461  seqovcd  10463  monoord2  10477  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  seq3f1olemqsum  10500  seq3f1o  10504  seq3distr  10513  expp1  10527  expcl2lemap  10532  expclzap  10545  expap0i  10552  nn0ltexp2  10689  bcval5  10743  hashinfuni  10757  hashennnuni  10759  hashnncl  10775  resunimafz0  10811  zfz1isolemiso  10819  zfz1isolem1  10820  zfz1iso  10821  seq3shft  10847  cvg1nlemcau  10993  rexanuz  10997  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  rersqreu  11037  caubnd2  11126  maxleast  11222  fimaxre2  11235  minmax  11238  xrmaxiflemcl  11253  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxadd  11269  xrminmax  11273  xrbdtri  11284  climreu  11305  reccn2ap  11321  iserex  11347  climcvg1nlem  11357  serf0  11360  fz1f1o  11383  summodclem3  11388  zsumdc  11392  fsum3  11395  isumz  11397  isumss  11399  isumss2  11401  fsumsersdc  11403  fsum3ser  11405  fsumsplit  11415  isumclim2  11430  isumclim3  11431  fsum2dlemstep  11442  fsumcnv  11445  fisumcom2  11446  bcxmas  11497  isumle  11503  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratz  11540  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  zproddc  11587  prod1dc  11594  fprodsplitdc  11604  fprodsplit  11605  fprodunsn  11612  fprodcl2lem  11613  fprodcllemf  11621  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  fprodle  11648  ef0lem  11668  mod2eq1n2dvds  11884  ndvdssub  11935  infssuzex  11950  infssuzcldc  11952  suprzubdc  11953  nninfdcex  11954  zsupssdc  11955  gcdsupex  11958  gcdsupcl  11959  bezoutlemnewy  11997  bezoutlemmain  11999  bezoutlembi  12006  bezoutlemeu  12008  bezoutlemle  12009  uzwodc  12038  nnwofdc  12039  nnwosdc  12040  nn0seqcvgd  12041  eucalgf  12055  eucalginv  12056  lcmval  12063  prmind2  12120  dfphi2  12220  phiprmpw  12222  phimullem  12225  eulerthlem1  12227  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  eulerth  12233  phisum  12240  odzcllem  12242  odzdvds  12245  pythagtriplem19  12282  pclemub  12287  pcprecl  12289  pceu  12295  pcqmul  12303  pcqcl  12306  pcxnn0cl  12310  pcge0  12312  pcdvdsb  12319  pceq0  12321  pcneg  12324  pcdvdstr  12326  pcgcd1  12327  pc2dvds  12329  pcz  12331  pcprmpw2  12332  pcaddlem  12338  pcadd  12339  pcmptcl  12340  pcmpt  12341  pcmptdvds  12343  fldivp1  12346  qexpz  12350  pockthlem  12354  pockthg  12355  prmunb  12360  1arith  12365  ennnfonelemom  12409  ennnfoneleminc  12412  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemdm  12421  ennnfonelemr  12424  ennnfonelemim  12425  exmidunben  12427  ctinfom  12429  inffinp1  12430  ctinf  12431  enctlem  12433  ctiunctlemu1st  12435  ctiunctlemu2nd  12436  ctiunctlemudc  12438  ctiunct  12441  ctiunctal  12442  unct  12443  ssomct  12446  nninfdclemcl  12449  nninfdclemp1  12451  nninfdc  12454  structcnvcnv  12478  setscom  12502  ressbas2d  12528  ressval3d  12531  ressabsg  12535  restid2  12697  imasaddfnlemg  12735  quslem  12745  ercpbl  12750  fnpr2ob  12759  mgmplusf  12785  grprinvlem  12804  grprinvd  12805  grpridd  12806  ismnd  12820  mhmpropd  12857  grppropd  12893  grpsubf  12949  dfgrp3mlem  12968  mulgnn0p1  12994  mulgnn0subcl  12996  mulgsubcl  12997  mulgneg  13001  mulgnn0dir  13013  mulgnn0ass  13019  issubg2m  13049  issubg4m  13053  lringuplu  13337  lmodscaf  13400  topontopon  13523  eltg3i  13559  epttop  13593  difopn  13611  uncld  13616  0nnei  13656  resttopon  13674  restabs  13678  restopnb  13684  lmcvg  13720  cnptopco  13725  cnss1  13729  cnss2  13730  cncnpi  13731  cncnp2m  13734  cnrest  13738  cnrest2  13739  cnrest2r  13740  cnptoprest  13742  cnptoprest2  13743  lmss  13749  lmff  13752  lmtopcnp  13753  lmcn  13754  txbasval  13770  upxp  13775  txcnmpt  13776  txdis1cn  13781  txlm  13782  lmcn2  13783  cnmpt11  13786  cnmpt11f  13787  cnmpt1t  13788  cnmpt12  13790  cnmpt21  13794  cnmpt21f  13795  cnmpt2t  13796  cnmpt22  13797  cnmpt22f  13798  cnmptcom  13801  hmeocnv  13810  hmeof1o  13812  hmeores  13818  txhmeo  13822  txswaphmeo  13824  isxmet2d  13851  blfvalps  13888  xblss2ps  13907  xblss2  13908  blfps  13912  blf  13913  unirnblps  13925  unirnbl  13926  isxms2  13955  bdxmet  14004  bdmet  14005  xmetxp  14010  xmettx  14013  blssioo  14048  tgioo  14049  mulcncflem  14093  dedekindeulemuub  14098  dedekindeulemub  14099  dedekindeulemloc  14100  dedekindeulemlu  14102  suplociccreex  14105  suplociccex  14106  dedekindicclemuub  14107  dedekindicclemub  14108  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemuopn  14119  limcrcl  14130  limcmpted  14135  limccnp2lem  14148  limccnp2cntop  14149  limccoap  14150  dvrecap  14180  cosordlem  14273  logbgcd1irraplemexp  14389  logbgcd1irrap  14391  lgsneg1  14429  lgsdilem  14431  lgsdir2  14437  lgsdirprm  14438  lgsdir  14439  lgsne0  14442  lgsabs1  14443  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem1  14453  2sqlem5  14469  2sqlem7  14471  2sqlem8a  14472  2sqlem8  14473  2sqlem9  14474  bj-stand  14503  bj-charfundcALT  14564  bj-charfunbi  14566  bj-bdfindis  14702  bj-peano4  14710  strcollnfALT  14741  pwtrufal  14750  pwf1oexmid  14752  subctctexmid  14753  pw1nct  14755  nnsf  14757  nninfalllem1  14760  nninfall  14761  nninfsellemqall  14767  exmidsbthrlem  14773  sbthom  14777  cvgcmp2nlemabs  14783  trilpo  14794  iswomni0  14802  redcwlpo  14806  dceqnconst  14810  dcapnconst  14811  nconstwlpolem  14815  nconstwlpo  14816  neapmkvlem  14817  neapmkv  14818  ltlenmkv  14820  taupi  14823  alsi1d  14831  alsi2d  14832  alsc1d  14833  alsc2d  14834