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  5364  fnimaeq0  5380  fnmpt  5385  fun2  5432  f00  5450  f0bi  5451  fimadmfo  5490  foimacnv  5523  resdif  5527  f1ococnv1  5534  fv3  5582  relelfvdm  5591  elfvm  5592  nfvres  5593  dffn5im  5607  mptfvex  5648  fvmptdf  5650  fvmptdv2  5652  fndmdif  5668  dff4im  5709  fmpt  5713  fmptd  5717  fmptdf  5720  f1oresrab  5728  fcoconst  5734  fsn  5735  ftpg  5747  fsnunf  5763  resfunexg  5784  isores1  5862  riota2df  5899  acexmidlemcase  5918  brabvv  5970  funoprabg  6023  fnovim  6033  ovmpodf  6056  ovi3  6062  elmpocl  6120  uchoice  6197  1stcof  6223  2ndcof  6224  fnmpo  6262  fmpoco  6276  fo2ndf  6287  f1o2ndf1  6288  disjxp1  6296  brtpos2  6311  reldmtpos  6313  dftpos3  6322  dftpos4  6323  tpostpos2  6325  tposf2  6328  tposf12  6329  tposfo  6331  tposf  6332  smores2  6354  tfrlem1  6368  tfrlem3-2d  6372  tfrlemisucaccv  6385  tfrlemibxssdm  6387  tfrlemibfn  6388  tfrlemi1  6392  tfrexlem  6394  tfr1onlemsucaccv  6401  tfr1onlembxssdm  6403  tfr1onlembfn  6404  tfr1onlemaccex  6408  tfrcllemsucaccv  6414  tfrcllembxssdm  6416  tfrcllembfn  6417  tfrcllemaccex  6421  tfrcldm  6423  rdgivallem  6441  rdgisucinc  6445  frecabex  6458  frecfnom  6461  frecfcllem  6464  frecsuclem  6466  omsuc  6532  nntri2  6554  nnsucuniel  6555  nnsseleq  6561  nnm00  6590  ecexr  6599  swoer  6622  elqsn0m  6664  iinerm  6668  erinxp  6670  ecinxp  6671  eroveu  6687  eroprf  6689  mapprc  6713  mapsn  6751  ixpprc  6780  ixp0  6792  resixp  6794  elixpsn  6796  dom2lem  6833  fundmen  6867  dom0  6901  xpf1o  6907  mapxpen  6911  xpmapenlem  6912  ssenen  6914  nneneq  6920  ssfilem  6938  dif1en  6942  dif1enen  6943  fin0  6948  fin0or  6949  diffitest  6950  diffisn  6956  ac6sfi  6961  fimax2gtrilemstep  6963  fimax2gtri  6964  finexdc  6965  exmidpweq  6972  pw1fin  6973  onunsnss  6980  unsnfidcel  6984  undifdcss  6986  undifdc  6987  tpfidceq  6993  fiintim  6994  fisseneq  6997  fidcenumlemr  7023  sbthlemi4  7028  sbthlemi5  7029  sbthlemi9  7033  fifo  7048  suplubti  7068  supelti  7070  infmoti  7096  infisoti  7100  djulclb  7123  updjud  7150  omp1eomlem  7162  0ct  7175  ctmlemr  7176  ctssdclemn0  7178  ctssdccl  7179  ctssdc  7181  enumct  7183  nninfninc  7191  nnnninfeq2  7197  finomni  7208  fodjuomnilemdc  7212  fodjum  7214  fodjuomnilemres  7216  fodjumkvlemres  7227  omniwomnimkv  7235  nninfwlporlem  7241  nninfwlpoimlemginf  7244  nninfwlpoim  7246  ficardon  7258  exmidonfinlem  7263  en2eleq  7265  exmidfodomrlemeldju  7269  exmidfodomrlemreseldju  7270  exmidfodomrlemim  7271  acfun  7277  exmidaclem  7278  exmidontriimlem3  7293  exmidontriimlem4  7294  exmidontriim  7295  pw1on  7296  dftap2  7321  2omotaplemst  7328  exmidapne  7330  ccfunen  7334  cc1  7335  cc2lem  7336  cc2  7337  cc3  7338  elni2  7384  indpi  7412  distrnqg  7457  subhalfnqq  7484  enq0sym  7502  enq0ref  7503  enq0tr  7504  nqnq0pi  7508  nnnq0lem1  7516  distrnq0  7529  elinp  7544  elnp1st2nd  7546  prltlu  7557  prnmaxl  7558  prnminu  7559  prarloc  7573  nqprm  7612  appdivnq  7633  prmuloc  7636  mullocpr  7641  distrlem4prl  7654  distrlem4pru  7655  ltexprlemm  7670  ltexprlemopl  7671  ltexprlemopu  7673  cauappcvgprlemopl  7716  cauappcvgprlemopu  7718  cauappcvgprlemdisj  7721  cauappcvgprlem2  7730  cauappcvgprlemlim  7731  caucvgprlemnkj  7736  caucvgprlemopl  7739  caucvgprlemopu  7741  caucvgprlemdisj  7744  caucvgprlemcl  7746  caucvgprlemladdfu  7747  caucvgprlemladdrl  7748  caucvgprlem2  7750  caucvgprprlemcbv  7757  caucvgprprlemval  7758  caucvgprprlemlol  7768  caucvgprprlemexbt  7776  caucvgprprlem1  7779  suplocexprlemrl  7787  suplocexprlemmu  7788  suplocexprlemru  7789  suplocexprlemdisj  7790  suplocexprlemloc  7791  suplocexprlemub  7793  suplocexprlemlub  7794  prsrlem1  7812  gt0srpr  7818  caucvgsrlemcl  7859  caucvgsrlembound  7864  caucvgsrlemgt1  7865  suplocsrlemb  7876  suplocsrlem  7878  suplocsr  7879  ltresr  7909  nnindnn  7963  axcaucvglemcl  7965  axcaucvglemval  7967  axcaucvglemcau  7968  axcaucvglemres  7969  axpre-suploclemres  7971  axpre-suploc  7972  sup3exmid  8987  nnind  9009  nn0supp  9304  nn0ge2m1nn  9312  zleloe  9376  zapne  9403  nn0lt2  9410  suprzclex  9427  zindd  9447  uzm1  9635  uzin  9637  infregelbex  9675  elnn1uz2  9684  nn01to3  9694  divfnzn  9698  qapne  9716  xrltnsym2  9872  xaddass  9947  xleadd1a  9951  xlt2add  9958  xlesubadd  9961  iooval2  9993  icoshftf1o  10069  fztri3or  10117  fzneuz  10179  4fvwrd4  10218  elfzo0  10261  infssuzex  10326  infssuzcldc  10328  suprzubdc  10329  nninfdcex  10330  zsupssdc  10331  exbtwnzlemex  10342  ioom  10353  fzfig  10525  uzennn  10531  uzsinds  10539  iseqovex  10553  seq3val  10555  seqvalcd  10556  seqf  10559  seqovcd  10562  monoord2  10581  iseqf1olemjpcl  10603  iseqf1olemqpcl  10604  seq3f1olemqsum  10608  seq3f1o  10612  seqf1og  10616  seq3distr  10627  expp1  10641  expcl2lemap  10646  expclzap  10659  expap0i  10666  nn0ltexp2  10804  bcval5  10858  hashinfuni  10872  hashennnuni  10874  hashnncl  10890  resunimafz0  10926  zfz1isolemiso  10934  zfz1isolem1  10935  zfz1iso  10936  wrdsymb0  10970  wrdlen1  10975  seq3shft  11006  cvg1nlemcau  11152  rexanuz  11156  resqrexlemoverl  11189  resqrexlemglsq  11190  resqrexlemsqa  11192  resqrexlemex  11193  rersqreu  11196  caubnd2  11285  maxleast  11381  fimaxre2  11395  minmax  11398  xrmaxiflemcl  11413  xrmaxiflemab  11415  xrmaxiflemlub  11416  xrmaxadd  11429  xrminmax  11433  xrbdtri  11444  climreu  11465  reccn2ap  11481  iserex  11507  climcvg1nlem  11517  serf0  11520  fz1f1o  11543  summodclem3  11548  zsumdc  11552  fsum3  11555  isumz  11557  isumss  11559  isumss2  11561  fsumsersdc  11563  fsum3ser  11565  fsumsplit  11575  isumclim2  11590  isumclim3  11591  fsum2dlemstep  11602  fsumcnv  11605  fisumcom2  11606  bcxmas  11657  isumle  11663  cvgratnnlemnexp  11692  cvgratnnlemmn  11693  cvgratz  11700  mertenslemub  11702  mertenslemi1  11703  mertenslem2  11704  mertensabs  11705  zproddc  11747  prod1dc  11754  fprodsplitdc  11764  fprodsplit  11765  fprodunsn  11772  fprodcl2lem  11773  fprodcllemf  11781  fprod2dlemstep  11790  fprodcnv  11793  fprodcom2fi  11794  fprodle  11808  ef0lem  11828  fsumdvds  12010  mod2eq1n2dvds  12047  ndvdssub  12098  bitsfzolem  12122  bitsfzo  12123  bitsinv1  12130  gcdsupex  12135  gcdsupcl  12136  bezoutlemnewy  12174  bezoutlemmain  12176  bezoutlembi  12183  bezoutlemeu  12185  bezoutlemle  12186  uzwodc  12215  nnwofdc  12216  nnwosdc  12217  nninfctlemfo  12218  nninfct  12219  nn0seqcvgd  12220  eucalgf  12234  eucalginv  12235  lcmval  12242  prmind2  12299  dfphi2  12399  phiprmpw  12401  phimullem  12404  eulerthlem1  12406  eulerthlemrprm  12408  eulerthlema  12409  eulerthlemh  12410  eulerthlemth  12411  eulerth  12412  phisum  12420  odzcllem  12422  odzdvds  12425  pythagtriplem19  12462  pclemub  12467  pcprecl  12469  pceu  12475  pcqmul  12483  pcqcl  12486  pcxnn0cl  12490  pcxqcl  12492  pcge0  12493  pcdvdsb  12500  pceq0  12502  pcneg  12505  pcdvdstr  12507  pcgcd1  12508  pc2dvds  12510  pcz  12512  pcprmpw2  12513  pcaddlem  12519  pcadd  12520  pcmptcl  12522  pcmpt  12523  pcmptdvds  12525  fldivp1  12528  qexpz  12532  pockthlem  12536  pockthg  12537  prmunb  12542  1arith  12547  4sqlemffi  12576  4sqlem17  12587  4sqlem18  12588  4sqlem19  12589  ennnfonelemom  12636  ennnfoneleminc  12639  ennnfonelemhf1o  12641  ennnfonelemex  12642  ennnfonelemhom  12643  ennnfonelemdm  12648  ennnfonelemr  12651  ennnfonelemim  12652  exmidunben  12654  ctinfom  12656  inffinp1  12657  ctinf  12658  enctlem  12660  ctiunctlemu1st  12662  ctiunctlemu2nd  12663  ctiunctlemudc  12665  ctiunct  12668  ctiunctal  12669  unct  12670  ssomct  12673  nninfdclemcl  12676  nninfdclemp1  12678  nninfdc  12681  structcnvcnv  12705  setscom  12729  relelbasov  12751  ressbas2d  12757  ressval3d  12761  ressabsg  12765  restid2  12936  imasaddfnlemg  12983  quslem  12993  ercpbl  13000  fnpr2ob  13009  mgmplusf  13035  grpinvalem  13054  grpinva  13055  grprida  13056  fngsum  13057  igsumvalx  13058  gsum0g  13065  gsumval2  13066  ismnd  13086  mhmpropd  13124  grppropd  13175  grpsubf  13237  dfgrp3mlem  13256  mulgnn0p1  13289  mulgnn0subcl  13291  mulgsubcl  13292  mulgneg  13296  mulgnn0dir  13308  mulgnn0ass  13314  submmulg  13322  issubg2m  13345  issubg4m  13349  ghmmulg  13412  ghmrn  13413  lringuplu  13778  lmodscaf  13892  lssintclm  13966  lspun0  14007  lidlbas  14060  topontopon  14282  eltg3i  14318  epttop  14352  difopn  14370  uncld  14375  0nnei  14415  resttopon  14433  restabs  14437  restopnb  14443  lmcvg  14479  cnptopco  14484  cnss1  14488  cnss2  14489  cncnpi  14490  cncnp2m  14493  cnrest  14497  cnrest2  14498  cnrest2r  14499  cnptoprest  14501  cnptoprest2  14502  lmss  14508  lmff  14511  lmtopcnp  14512  lmcn  14513  txbasval  14529  upxp  14534  txcnmpt  14535  txdis1cn  14540  txlm  14541  lmcn2  14542  cnmpt11  14545  cnmpt11f  14546  cnmpt1t  14547  cnmpt12  14549  cnmpt21  14553  cnmpt21f  14554  cnmpt2t  14555  cnmpt22  14556  cnmpt22f  14557  cnmptcom  14560  hmeocnv  14569  hmeof1o  14571  hmeores  14577  txhmeo  14581  txswaphmeo  14583  isxmet2d  14610  blfvalps  14647  xblss2ps  14666  xblss2  14667  blfps  14671  blf  14672  unirnblps  14684  unirnbl  14685  isxms2  14714  bdxmet  14763  bdmet  14764  xmetxp  14769  xmettx  14772  blssioo  14815  tgioo  14816  mulcncflem  14869  divcncfap  14876  dedekindeulemuub  14879  dedekindeulemub  14880  dedekindeulemloc  14881  dedekindeulemlu  14883  suplociccreex  14886  suplociccex  14887  dedekindicclemuub  14888  dedekindicclemub  14889  dedekindicclemloc  14890  dedekindicclemlu  14892  dedekindicc  14895  ivthinclemlopn  14898  ivthinclemuopn  14900  ivthdich  14915  limcrcl  14920  limcmpted  14925  limccnp2lem  14938  limccnp2cntop  14939  limccoap  14940  dvrecap  14975  plyaddlem1  15009  plymullem1  15010  plycoeid3  15019  plyco  15021  plycj  15023  plyrecj  15025  dvply1  15027  dvply2g  15028  cosordlem  15111  logbgcd1irraplemexp  15230  logbgcd1irrap  15232  lgsneg1  15292  lgsdilem  15294  lgsdir2  15300  lgsdirprm  15301  lgsdir  15302  lgsne0  15305  lgsabs1  15306  lgsdirnn0  15314  lgsdinn0  15315  gausslemma2dlem1f1o  15327  gausslemma2dlem4  15331  lgseisenlem1  15337  lgsquadlem3  15346  2lgslem1a  15355  2sqlem5  15386  2sqlem7  15388  2sqlem8a  15389  2sqlem8  15390  2sqlem9  15391  bj-stand  15420  bj-charfundcALT  15481  bj-charfunbi  15483  bj-bdfindis  15619  bj-peano4  15627  strcollnfALT  15658  1dom1el  15663  2omap  15668  pwtrufal  15670  pwf1oexmid  15672  subctctexmid  15673  pw1nct  15676  nnsf  15678  nninfalllem1  15681  nninfall  15682  nninfsellemqall  15688  nnnninfen  15694  exmidsbthrlem  15695  sbthom  15699  cvgcmp2nlemabs  15705  trilpo  15716  iswomni0  15724  redcwlpo  15728  dceqnconst  15733  dcapnconst  15734  nconstwlpolem  15738  nconstwlpo  15739  neapmkvlem  15740  neapmkv  15741  ltlenmkv  15743  taupi  15746  alsi1d  15754  alsi2d  15755  alsc1d  15756  alsc2d  15757