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  1607  nexd  1624  alexnim  1659  excomim  1674  19.41  1697  equcomd  1718  nfexd  1772  sbh  1787  sbcof2  1821  sbidm  1862  sb6rf  1864  nfsbt  1992  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  eu2  2086  2euex  2129  eqcomd  2199  3eltr3g  2278  abbid  2310  neneqd  2385  eqnetrrid  2395  3netr3g  2398  necomd  2450  r19.21bi  2582  nrexdv  2587  rexlimd  2608  rabbidva  2748  elisset  2774  euind  2948  rmoan  2961  reuind  2966  2rmorex  2967  spsbc  2998  spesbc  3072  eldifad  3165  eldifbd  3166  3sstr3g  3222  sseqtrdi  3228  difindiss  3414  un00  3494  undifss  3528  ifcldcd  3594  disjpr2  3683  difprsn1  3758  diftpsn3  3760  difsnss  3765  sneqr  3787  preqr1  3795  preq12b  3797  oprcl  3829  intab  3900  riinm  3986  rintm  4006  disjiun  4025  sndisj  4026  3brtr3g  4063  trint  4143  iinexgm  4184  exmidexmid  4226  exmid01  4228  pwntru  4229  exmid1stab  4238  pwel  4248  exss  4257  0nelop  4278  euotd  4284  opelopabsb  4291  pwunim  4318  issod  4351  frind  4384  suctr  4453  orduniss  4457  onelini  4462  oneluni  4463  eusv2i  4487  rexxfrd  4495  rabxfrd  4501  reuhypd  4503  iunpw  4512  sucexg  4531  ordsucim  4533  ordtriexmidlem  4552  ontriexmidim  4555  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  ordsucunielexmid  4564  orddif  4580  suc11g  4590  onintexmid  4606  reg3exmidlemwe  4612  tfisi  4620  peano1  4627  peano2  4628  finds2  4634  omsinds  4655  brrelex12  4698  brel  4712  ssrel  4748  ssrel2  4750  ssrelrel  4760  elrel  4762  xpsspw  4772  relop  4813  dmxpm  4883  opelresi  4954  mptimass  5019  ndmima  5043  poirr2  5059  xpmlem  5087  xpimasn  5115  iotass  5233  iotacl  5240  dffun5r  5267  funeu  5280  funeu2  5281  funfnd  5286  funopg  5289  funun  5299  funinsn  5304  funtp  5308  funcnvuni  5324  funcnvres2  5330  imadiflem  5334  imadif  5335  funimaexglem  5338  fneu2  5360  fnimaeq0  5376  fnmpt  5381  fun2  5428  f00  5446  f0bi  5447  fimadmfo  5486  foimacnv  5519  resdif  5523  f1ococnv1  5530  fv3  5578  relelfvdm  5587  elfvm  5588  nfvres  5589  dffn5im  5603  mptfvex  5644  fvmptdf  5646  fvmptdv2  5648  fndmdif  5664  dff4im  5705  fmpt  5709  fmptd  5713  fmptdf  5716  f1oresrab  5724  fcoconst  5730  fsn  5731  ftpg  5743  fsnunf  5759  resfunexg  5780  isores1  5858  riota2df  5895  acexmidlemcase  5914  brabvv  5965  funoprabg  6018  fnovim  6028  ovmpodf  6051  ovi3  6057  elmpocl  6115  uchoice  6192  1stcof  6218  2ndcof  6219  fnmpo  6257  fmpoco  6271  fo2ndf  6282  f1o2ndf1  6283  disjxp1  6291  brtpos2  6306  reldmtpos  6308  dftpos3  6317  dftpos4  6318  tpostpos2  6320  tposf2  6323  tposf12  6324  tposfo  6326  tposf  6327  smores2  6349  tfrlem1  6363  tfrlem3-2d  6367  tfrlemisucaccv  6380  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrlemi1  6387  tfrexlem  6389  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  tfrcldm  6418  rdgivallem  6436  rdgisucinc  6440  frecabex  6453  frecfnom  6456  frecfcllem  6459  frecsuclem  6461  omsuc  6527  nntri2  6549  nnsucuniel  6550  nnsseleq  6556  nnm00  6585  ecexr  6594  swoer  6617  elqsn0m  6659  iinerm  6663  erinxp  6665  ecinxp  6666  eroveu  6682  eroprf  6684  mapprc  6708  mapsn  6746  ixpprc  6775  ixp0  6787  resixp  6789  elixpsn  6791  dom2lem  6828  fundmen  6862  dom0  6896  xpf1o  6902  mapxpen  6906  xpmapenlem  6907  ssenen  6909  nneneq  6915  ssfilem  6933  dif1en  6937  dif1enen  6938  fin0  6943  fin0or  6944  diffitest  6945  diffisn  6951  ac6sfi  6956  fimax2gtrilemstep  6958  fimax2gtri  6959  finexdc  6960  exmidpweq  6967  pw1fin  6968  onunsnss  6975  unsnfidcel  6979  undifdcss  6981  undifdc  6982  fiintim  6987  fisseneq  6990  fidcenumlemr  7016  sbthlemi4  7021  sbthlemi5  7022  sbthlemi9  7026  fifo  7041  suplubti  7061  supelti  7063  infmoti  7089  infisoti  7093  djulclb  7116  updjud  7143  omp1eomlem  7155  0ct  7168  ctmlemr  7169  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumct  7176  nninfninc  7184  nnnninfeq2  7190  finomni  7201  fodjuomnilemdc  7205  fodjum  7207  fodjuomnilemres  7209  fodjumkvlemres  7220  omniwomnimkv  7228  nninfwlporlem  7234  nninfwlpoimlemginf  7237  nninfwlpoim  7239  exmidonfinlem  7255  en2eleq  7257  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  exmidfodomrlemim  7263  acfun  7269  exmidaclem  7270  exmidontriimlem3  7285  exmidontriimlem4  7286  exmidontriim  7287  pw1on  7288  dftap2  7313  2omotaplemst  7320  exmidapne  7322  ccfunen  7326  cc1  7327  cc2lem  7328  cc2  7329  cc3  7330  elni2  7376  indpi  7404  distrnqg  7449  subhalfnqq  7476  enq0sym  7494  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  nnnq0lem1  7508  distrnq0  7521  elinp  7536  elnp1st2nd  7538  prltlu  7549  prnmaxl  7550  prnminu  7551  prarloc  7565  nqprm  7604  appdivnq  7625  prmuloc  7628  mullocpr  7633  distrlem4prl  7646  distrlem4pru  7647  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlemdisj  7713  cauappcvgprlem2  7722  cauappcvgprlemlim  7723  caucvgprlemnkj  7728  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlemdisj  7736  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem2  7742  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemlol  7760  caucvgprprlemexbt  7768  caucvgprprlem1  7771  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  prsrlem1  7804  gt0srpr  7810  caucvgsrlemcl  7851  caucvgsrlembound  7856  caucvgsrlemgt1  7857  suplocsrlemb  7868  suplocsrlem  7870  suplocsr  7871  ltresr  7901  nnindnn  7955  axcaucvglemcl  7957  axcaucvglemval  7959  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  sup3exmid  8978  nnind  9000  nn0supp  9295  nn0ge2m1nn  9303  zleloe  9367  zapne  9394  nn0lt2  9401  suprzclex  9418  zindd  9438  uzm1  9626  uzin  9628  infregelbex  9666  elnn1uz2  9675  nn01to3  9685  divfnzn  9689  qapne  9707  xrltnsym2  9863  xaddass  9938  xleadd1a  9942  xlt2add  9949  xlesubadd  9952  iooval2  9984  icoshftf1o  10060  fztri3or  10108  fzneuz  10170  4fvwrd4  10209  elfzo0  10252  exbtwnzlemex  10321  ioom  10332  fzfig  10504  uzennn  10510  uzsinds  10518  iseqovex  10532  seq3val  10534  seqvalcd  10535  seqf  10538  seqovcd  10541  monoord2  10560  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  seq3f1olemqsum  10587  seq3f1o  10591  seqf1og  10595  seq3distr  10606  expp1  10620  expcl2lemap  10625  expclzap  10638  expap0i  10645  nn0ltexp2  10783  bcval5  10837  hashinfuni  10851  hashennnuni  10853  hashnncl  10869  resunimafz0  10905  zfz1isolemiso  10913  zfz1isolem1  10914  zfz1iso  10915  wrdsymb0  10949  wrdlen1  10954  seq3shft  10985  cvg1nlemcau  11131  rexanuz  11135  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  rersqreu  11175  caubnd2  11264  maxleast  11360  fimaxre2  11373  minmax  11376  xrmaxiflemcl  11391  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxadd  11407  xrminmax  11411  xrbdtri  11422  climreu  11443  reccn2ap  11459  iserex  11485  climcvg1nlem  11495  serf0  11498  fz1f1o  11521  summodclem3  11526  zsumdc  11530  fsum3  11533  isumz  11535  isumss  11537  isumss2  11539  fsumsersdc  11541  fsum3ser  11543  fsumsplit  11553  isumclim2  11568  isumclim3  11569  fsum2dlemstep  11580  fsumcnv  11583  fisumcom2  11584  bcxmas  11635  isumle  11641  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  zproddc  11725  prod1dc  11732  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  fprodcl2lem  11751  fprodcllemf  11759  fprod2dlemstep  11768  fprodcnv  11771  fprodcom2fi  11772  fprodle  11786  ef0lem  11806  mod2eq1n2dvds  12023  ndvdssub  12074  infssuzex  12089  infssuzcldc  12091  suprzubdc  12092  nninfdcex  12093  zsupssdc  12094  gcdsupex  12097  gcdsupcl  12098  bezoutlemnewy  12136  bezoutlemmain  12138  bezoutlembi  12145  bezoutlemeu  12147  bezoutlemle  12148  uzwodc  12177  nnwofdc  12178  nnwosdc  12179  nninfctlemfo  12180  nninfct  12181  nn0seqcvgd  12182  eucalgf  12196  eucalginv  12197  lcmval  12204  prmind2  12261  dfphi2  12361  phiprmpw  12363  phimullem  12366  eulerthlem1  12368  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  eulerth  12374  phisum  12381  odzcllem  12383  odzdvds  12386  pythagtriplem19  12423  pclemub  12428  pcprecl  12430  pceu  12436  pcqmul  12444  pcqcl  12447  pcxnn0cl  12451  pcxqcl  12453  pcge0  12454  pcdvdsb  12461  pceq0  12463  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  pcz  12473  pcprmpw2  12474  pcaddlem  12480  pcadd  12481  pcmptcl  12483  pcmpt  12484  pcmptdvds  12486  fldivp1  12489  qexpz  12493  pockthlem  12497  pockthg  12498  prmunb  12503  1arith  12508  4sqlemffi  12537  4sqlem17  12548  4sqlem18  12549  4sqlem19  12550  ennnfonelemom  12568  ennnfoneleminc  12571  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemdm  12580  ennnfonelemr  12583  ennnfonelemim  12584  exmidunben  12586  ctinfom  12588  inffinp1  12589  ctinf  12590  enctlem  12592  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  ctiunctlemudc  12597  ctiunct  12600  ctiunctal  12601  unct  12602  ssomct  12605  nninfdclemcl  12608  nninfdclemp1  12610  nninfdc  12613  structcnvcnv  12637  setscom  12661  relelbasov  12683  ressbas2d  12689  ressval3d  12693  ressabsg  12697  restid2  12862  imasaddfnlemg  12900  quslem  12910  ercpbl  12917  fnpr2ob  12926  mgmplusf  12952  grpinvalem  12971  grpinva  12972  grprida  12973  fngsum  12974  igsumvalx  12975  gsum0g  12982  gsumval2  12983  ismnd  13003  mhmpropd  13041  grppropd  13092  grpsubf  13154  dfgrp3mlem  13173  mulgnn0p1  13206  mulgnn0subcl  13208  mulgsubcl  13209  mulgneg  13213  mulgnn0dir  13225  mulgnn0ass  13231  submmulg  13239  issubg2m  13262  issubg4m  13266  ghmmulg  13329  ghmrn  13330  lringuplu  13695  lmodscaf  13809  lssintclm  13883  lspun0  13924  lidlbas  13977  topontopon  14199  eltg3i  14235  epttop  14269  difopn  14287  uncld  14292  0nnei  14332  resttopon  14350  restabs  14354  restopnb  14360  lmcvg  14396  cnptopco  14401  cnss1  14405  cnss2  14406  cncnpi  14407  cncnp2m  14410  cnrest  14414  cnrest2  14415  cnrest2r  14416  cnptoprest  14418  cnptoprest2  14419  lmss  14425  lmff  14428  lmtopcnp  14429  lmcn  14430  txbasval  14446  upxp  14451  txcnmpt  14452  txdis1cn  14457  txlm  14458  lmcn2  14459  cnmpt11  14462  cnmpt11f  14463  cnmpt1t  14464  cnmpt12  14466  cnmpt21  14470  cnmpt21f  14471  cnmpt2t  14472  cnmpt22  14473  cnmpt22f  14474  cnmptcom  14477  hmeocnv  14486  hmeof1o  14488  hmeores  14494  txhmeo  14498  txswaphmeo  14500  isxmet2d  14527  blfvalps  14564  xblss2ps  14583  xblss2  14584  blfps  14588  blf  14589  unirnblps  14601  unirnbl  14602  isxms2  14631  bdxmet  14680  bdmet  14681  xmetxp  14686  xmettx  14689  blssioo  14732  tgioo  14733  mulcncflem  14786  divcncfap  14793  dedekindeulemuub  14796  dedekindeulemub  14797  dedekindeulemloc  14798  dedekindeulemlu  14800  suplociccreex  14803  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemub  14806  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthdich  14832  limcrcl  14837  limcmpted  14842  limccnp2lem  14855  limccnp2cntop  14856  limccoap  14857  dvrecap  14892  plyaddlem1  14926  plymullem1  14927  plyco  14937  plycj  14939  plyrecj  14941  dvply1  14943  cosordlem  15025  logbgcd1irraplemexp  15141  logbgcd1irrap  15143  lgsneg1  15182  lgsdilem  15184  lgsdir2  15190  lgsdirprm  15191  lgsdir  15192  lgsne0  15195  lgsabs1  15196  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1f1o  15217  gausslemma2dlem4  15221  lgseisenlem1  15227  lgsquadlem3  15236  2lgslem1a  15245  2sqlem5  15276  2sqlem7  15278  2sqlem8a  15279  2sqlem8  15280  2sqlem9  15281  bj-stand  15310  bj-charfundcALT  15371  bj-charfunbi  15373  bj-bdfindis  15509  bj-peano4  15517  strcollnfALT  15548  1dom1el  15553  pwtrufal  15558  pwf1oexmid  15560  subctctexmid  15561  pw1nct  15563  nnsf  15565  nninfalllem1  15568  nninfall  15569  nninfsellemqall  15575  nnnninfen  15581  exmidsbthrlem  15582  sbthom  15586  cvgcmp2nlemabs  15592  trilpo  15603  iswomni0  15611  redcwlpo  15615  dceqnconst  15620  dcapnconst  15621  nconstwlpolem  15625  nconstwlpo  15626  neapmkvlem  15627  neapmkv  15628  ltlenmkv  15630  taupi  15633  alsi1d  15641  alsi2d  15642  alsc1d  15643  alsc2d  15644