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  731  3mix3  1171  mpjao3dan  1320  ecase23d  1363  exlimdh  1620  nexd  1637  alexnim  1672  excomim  1687  19.41  1710  equcomd  1731  nfexd  1785  sbh  1800  sbcof2  1834  sbidm  1875  sb6rf  1877  nfsbt  2005  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  eu2  2099  2euex  2142  eqcomd  2212  3eltr3g  2291  abbid  2323  neneqd  2398  eqnetrrid  2408  3netr3g  2411  necomd  2463  r19.21bi  2595  nrexdv  2600  rexlimd  2621  rabbidva  2761  elisset  2788  euind  2964  rmoan  2977  reuind  2982  2rmorex  2983  spsbc  3014  spesbc  3088  eldifad  3181  eldifbd  3182  3sstr3g  3239  sseqtrdi  3245  difindiss  3431  un00  3511  undifss  3545  ifcldcd  3612  disjpr2  3701  difprsn1  3777  diftpsn3  3779  difsnss  3784  sneqr  3806  preqr1  3814  preq12b  3816  oprcl  3848  intab  3919  riinm  4005  rintm  4025  disjiun  4045  sndisj  4046  3brtr3g  4083  trint  4164  iinexgm  4205  exmidexmid  4247  exmid01  4249  pwntru  4250  exmid1stab  4259  pwel  4269  exss  4278  0nelop  4299  euotd  4306  opelopabsb  4313  pwunim  4340  issod  4373  frind  4406  suctr  4475  orduniss  4479  onelini  4484  oneluni  4485  eusv2i  4509  rexxfrd  4517  rabxfrd  4523  reuhypd  4525  iunpw  4534  sucexg  4553  ordsucim  4555  ordtriexmidlem  4574  ontriexmidim  4577  ordtri2or2exmidlem  4581  onsucelsucexmidlem  4584  ordsucunielexmid  4586  orddif  4602  suc11g  4612  onintexmid  4628  reg3exmidlemwe  4634  tfisi  4642  peano1  4649  peano2  4650  finds2  4656  omsinds  4677  brrelex12  4720  brel  4734  ssrel  4770  ssrel2  4772  ssrelrel  4782  elrel  4784  xpsspw  4794  relop  4835  dmxpm  4906  opelresi  4978  mptimass  5043  ndmima  5067  poirr2  5083  xpmlem  5111  xpimasn  5139  iotass  5257  iotacl  5264  dffun5r  5291  funeu  5304  funeu2  5305  funfnd  5310  funopg  5313  funun  5323  fununfun  5325  funinsn  5331  funtp  5335  funcnvuni  5351  funcnvres2  5357  imadiflem  5361  imadif  5362  funimaexglem  5365  fneu2  5389  fnimaeq0  5406  fnmpt  5411  fun2  5459  f00  5478  f0bi  5479  fimadmfo  5518  foimacnv  5551  resdif  5555  f1ococnv1  5562  fv3  5611  relelfvdm  5620  elfvm  5621  nfvres  5622  dffn5im  5636  mptfvex  5677  fvmptdf  5679  fvmptdv2  5681  fndmdif  5697  dff4im  5738  fmpt  5742  fmptd  5746  fmptdf  5749  f1oresrab  5757  fcoconst  5763  fsn  5764  funopsn  5774  ftpg  5780  fsnunf  5796  resfunexg  5817  isores1  5895  riota2df  5932  acexmidlemcase  5951  brabvv  6003  funoprabg  6056  fnovim  6066  ovmpodf  6089  ovi3  6095  elmpocl  6153  uchoice  6235  1stcof  6261  2ndcof  6262  fnmpo  6300  fmpoco  6314  fo2ndf  6325  f1o2ndf1  6326  disjxp1  6334  brtpos2  6349  reldmtpos  6351  dftpos3  6360  dftpos4  6361  tpostpos2  6363  tposf2  6366  tposf12  6367  tposfo  6369  tposf  6370  smores2  6392  tfrlem1  6406  tfrlem3-2d  6410  tfrlemisucaccv  6423  tfrlemibxssdm  6425  tfrlemibfn  6426  tfrlemi1  6430  tfrexlem  6432  tfr1onlemsucaccv  6439  tfr1onlembxssdm  6441  tfr1onlembfn  6442  tfr1onlemaccex  6446  tfrcllemsucaccv  6452  tfrcllembxssdm  6454  tfrcllembfn  6455  tfrcllemaccex  6459  tfrcldm  6461  rdgivallem  6479  rdgisucinc  6483  frecabex  6496  frecfnom  6499  frecfcllem  6502  frecsuclem  6504  omsuc  6570  nntri2  6592  nnsucuniel  6593  nnsseleq  6599  nnm00  6628  ecexr  6637  swoer  6660  elqsn0m  6702  iinerm  6706  erinxp  6708  ecinxp  6709  eroveu  6725  eroprf  6727  mapprc  6751  mapsn  6789  ixpprc  6818  ixp0  6830  resixp  6832  elixpsn  6834  dom2lem  6875  fundmen  6911  dom0  6949  xpf1o  6955  mapxpen  6959  xpmapenlem  6960  ssenen  6962  nneneq  6968  ssfilem  6986  dif1en  6990  dif1enen  6991  fin0  6996  fin0or  6997  diffitest  6998  diffisn  7004  ac6sfi  7009  fimax2gtrilemstep  7011  fimax2gtri  7012  finexdc  7013  exmidpweq  7020  pw1fin  7021  onunsnss  7028  unsnfidcel  7032  undifdcss  7034  undifdc  7035  tpfidceq  7041  fiintim  7042  fisseneq  7045  fidcenumlemr  7071  sbthlemi4  7076  sbthlemi5  7077  sbthlemi9  7081  fifo  7096  suplubti  7116  supelti  7118  infmoti  7144  infisoti  7148  djulclb  7171  updjud  7198  omp1eomlem  7210  0ct  7223  ctmlemr  7224  ctssdclemn0  7226  ctssdccl  7227  ctssdc  7229  enumct  7231  nninfninc  7239  nnnninfeq2  7245  finomni  7256  fodjuomnilemdc  7260  fodjum  7262  fodjuomnilemres  7264  fodjumkvlemres  7275  omniwomnimkv  7283  nninfwlporlem  7289  nninfwlpoimlemginf  7292  nninfwlpoim  7295  nninfinfwlpo  7296  ficardon  7310  exmidonfinlem  7316  en2eleq  7318  exmidfodomrlemeldju  7322  exmidfodomrlemreseldju  7323  exmidfodomrlemim  7324  finacn  7331  acfun  7334  exmidaclem  7335  exmidontriimlem3  7350  exmidontriimlem4  7351  exmidontriim  7352  pw1on  7353  dftap2  7378  2omotaplemst  7385  exmidapne  7387  ccfunen  7391  cc1  7392  cc2lem  7393  cc2  7394  cc3  7395  acnccim  7399  elni2  7442  indpi  7470  distrnqg  7515  subhalfnqq  7542  enq0sym  7560  enq0ref  7561  enq0tr  7562  nqnq0pi  7566  nnnq0lem1  7574  distrnq0  7587  elinp  7602  elnp1st2nd  7604  prltlu  7615  prnmaxl  7616  prnminu  7617  prarloc  7631  nqprm  7670  appdivnq  7691  prmuloc  7694  mullocpr  7699  distrlem4prl  7712  distrlem4pru  7713  ltexprlemm  7728  ltexprlemopl  7729  ltexprlemopu  7731  cauappcvgprlemopl  7774  cauappcvgprlemopu  7776  cauappcvgprlemdisj  7779  cauappcvgprlem2  7788  cauappcvgprlemlim  7789  caucvgprlemnkj  7794  caucvgprlemopl  7797  caucvgprlemopu  7799  caucvgprlemdisj  7802  caucvgprlemcl  7804  caucvgprlemladdfu  7805  caucvgprlemladdrl  7806  caucvgprlem2  7808  caucvgprprlemcbv  7815  caucvgprprlemval  7816  caucvgprprlemlol  7826  caucvgprprlemexbt  7834  caucvgprprlem1  7837  suplocexprlemrl  7845  suplocexprlemmu  7846  suplocexprlemru  7847  suplocexprlemdisj  7848  suplocexprlemloc  7849  suplocexprlemub  7851  suplocexprlemlub  7852  prsrlem1  7870  gt0srpr  7876  caucvgsrlemcl  7917  caucvgsrlembound  7922  caucvgsrlemgt1  7923  suplocsrlemb  7934  suplocsrlem  7936  suplocsr  7937  ltresr  7967  nnindnn  8021  axcaucvglemcl  8023  axcaucvglemval  8025  axcaucvglemcau  8026  axcaucvglemres  8027  axpre-suploclemres  8029  axpre-suploc  8030  sup3exmid  9045  nnind  9067  nn0supp  9362  nn0ge2m1nn  9370  zleloe  9434  zapne  9462  nn0lt2  9469  suprzclex  9486  zindd  9506  uzm1  9694  uzin  9696  infregelbex  9734  elnn1uz2  9743  nn01to3  9753  divfnzn  9757  qapne  9775  xrltnsym2  9931  xaddass  10006  xleadd1a  10010  xlt2add  10017  xlesubadd  10020  iooval2  10052  icoshftf1o  10128  fztri3or  10176  fzneuz  10238  4fvwrd4  10277  elfzo0  10323  infssuzex  10393  infssuzcldc  10395  suprzubdc  10396  nninfdcex  10397  zsupssdc  10398  exbtwnzlemex  10409  ioom  10420  fzfig  10592  uzennn  10598  uzsinds  10606  iseqovex  10620  seq3val  10622  seqvalcd  10623  seqf  10626  seqovcd  10629  monoord2  10648  iseqf1olemjpcl  10670  iseqf1olemqpcl  10671  seq3f1olemqsum  10675  seq3f1o  10679  seqf1og  10683  seq3distr  10694  expp1  10708  expcl2lemap  10713  expclzap  10726  expap0i  10733  nn0ltexp2  10871  bcval5  10925  hashinfuni  10939  hashennnuni  10941  hashnncl  10957  resunimafz0  10993  zfz1isolemiso  11001  zfz1isolem1  11002  zfz1iso  11003  wrdsymb0  11043  wrdlen1  11048  ccat1st1st  11111  swrdrlen  11132  pfxid  11157  pfxwrdsymbg  11161  pfxtrcfv  11164  pfxccat1  11173  pfxpfxid  11180  pfxcctswrd  11181  seq3shft  11219  cvg1nlemcau  11365  rexanuz  11369  resqrexlemoverl  11402  resqrexlemglsq  11403  resqrexlemsqa  11405  resqrexlemex  11406  rersqreu  11409  caubnd2  11498  maxleast  11594  fimaxre2  11608  minmax  11611  xrmaxiflemcl  11626  xrmaxiflemab  11628  xrmaxiflemlub  11629  xrmaxadd  11642  xrminmax  11646  xrbdtri  11657  climreu  11678  reccn2ap  11694  iserex  11720  climcvg1nlem  11730  serf0  11733  fz1f1o  11756  summodclem3  11761  zsumdc  11765  fsum3  11768  isumz  11770  isumss  11772  isumss2  11774  fsumsersdc  11776  fsum3ser  11778  fsumsplit  11788  isumclim2  11803  isumclim3  11804  fsum2dlemstep  11815  fsumcnv  11818  fisumcom2  11819  bcxmas  11870  isumle  11876  cvgratnnlemnexp  11905  cvgratnnlemmn  11906  cvgratz  11913  mertenslemub  11915  mertenslemi1  11916  mertenslem2  11917  mertensabs  11918  zproddc  11960  prod1dc  11967  fprodsplitdc  11977  fprodsplit  11978  fprodunsn  11985  fprodcl2lem  11986  fprodcllemf  11994  fprod2dlemstep  12003  fprodcnv  12006  fprodcom2fi  12007  fprodle  12021  ef0lem  12041  fsumdvds  12223  mod2eq1n2dvds  12260  ndvdssub  12311  bitsfzolem  12335  bitsfzo  12336  bitsinv1  12343  gcdsupex  12348  gcdsupcl  12349  bezoutlemnewy  12387  bezoutlemmain  12389  bezoutlembi  12396  bezoutlemeu  12398  bezoutlemle  12399  uzwodc  12428  nnwofdc  12429  nnwosdc  12430  nninfctlemfo  12431  nninfct  12432  nn0seqcvgd  12433  eucalgf  12447  eucalginv  12448  lcmval  12455  prmind2  12512  dfphi2  12612  phiprmpw  12614  phimullem  12617  eulerthlem1  12619  eulerthlemrprm  12621  eulerthlema  12622  eulerthlemh  12623  eulerthlemth  12624  eulerth  12625  phisum  12633  odzcllem  12635  odzdvds  12638  pythagtriplem19  12675  pclemub  12680  pcprecl  12682  pceu  12688  pcqmul  12696  pcqcl  12699  pcxnn0cl  12703  pcxqcl  12705  pcge0  12706  pcdvdsb  12713  pceq0  12715  pcneg  12718  pcdvdstr  12720  pcgcd1  12721  pc2dvds  12723  pcz  12725  pcprmpw2  12726  pcaddlem  12732  pcadd  12733  pcmptcl  12735  pcmpt  12736  pcmptdvds  12738  fldivp1  12741  qexpz  12745  pockthlem  12749  pockthg  12750  prmunb  12755  1arith  12760  4sqlemffi  12789  4sqlem17  12800  4sqlem18  12801  4sqlem19  12802  ennnfonelemom  12849  ennnfoneleminc  12852  ennnfonelemhf1o  12854  ennnfonelemex  12855  ennnfonelemhom  12856  ennnfonelemdm  12861  ennnfonelemr  12864  ennnfonelemim  12865  exmidunben  12867  ctinfom  12869  inffinp1  12870  ctinf  12871  enctlem  12873  ctiunctlemu1st  12875  ctiunctlemu2nd  12876  ctiunctlemudc  12878  ctiunct  12881  ctiunctal  12882  unct  12883  ssomct  12886  nninfdclemcl  12889  nninfdclemp1  12891  nninfdc  12894  structcnvcnv  12918  setscom  12942  relelbasov  12964  ressbas2d  12970  ressval3d  12974  ressabsg  12978  restid2  13150  imasaddfnlemg  13216  quslem  13226  ercpbl  13233  fnpr2ob  13242  mgmplusf  13268  grpinvalem  13287  grpinva  13288  grprida  13289  fngsum  13290  igsumvalx  13291  gsum0g  13298  gsumval2  13299  ismnd  13321  mhmpropd  13368  grppropd  13419  grpsubf  13481  dfgrp3mlem  13500  mulgnn0p1  13539  mulgnn0subcl  13541  mulgsubcl  13542  mulgneg  13546  mulgnn0dir  13558  mulgnn0ass  13564  submmulg  13572  issubg2m  13595  issubg4m  13599  ghmmulg  13662  ghmrn  13663  lringuplu  14028  lmodscaf  14142  lssintclm  14216  lspun0  14257  lidlbas  14310  psr1clfi  14520  topontopon  14562  eltg3i  14598  epttop  14632  difopn  14650  uncld  14655  0nnei  14695  resttopon  14713  restabs  14717  restopnb  14723  lmcvg  14759  cnptopco  14764  cnss1  14768  cnss2  14769  cncnpi  14770  cncnp2m  14773  cnrest  14777  cnrest2  14778  cnrest2r  14779  cnptoprest  14781  cnptoprest2  14782  lmss  14788  lmff  14791  lmtopcnp  14792  lmcn  14793  txbasval  14809  upxp  14814  txcnmpt  14815  txdis1cn  14820  txlm  14821  lmcn2  14822  cnmpt11  14825  cnmpt11f  14826  cnmpt1t  14827  cnmpt12  14829  cnmpt21  14833  cnmpt21f  14834  cnmpt2t  14835  cnmpt22  14836  cnmpt22f  14837  cnmptcom  14840  hmeocnv  14849  hmeof1o  14851  hmeores  14857  txhmeo  14861  txswaphmeo  14863  isxmet2d  14890  blfvalps  14927  xblss2ps  14946  xblss2  14947  blfps  14951  blf  14952  unirnblps  14964  unirnbl  14965  isxms2  14994  bdxmet  15043  bdmet  15044  xmetxp  15049  xmettx  15052  blssioo  15095  tgioo  15096  mulcncflem  15149  divcncfap  15156  dedekindeulemuub  15159  dedekindeulemub  15160  dedekindeulemloc  15161  dedekindeulemlu  15163  suplociccreex  15166  suplociccex  15167  dedekindicclemuub  15168  dedekindicclemub  15169  dedekindicclemloc  15170  dedekindicclemlu  15172  dedekindicc  15175  ivthinclemlopn  15178  ivthinclemuopn  15180  ivthdich  15195  limcrcl  15200  limcmpted  15205  limccnp2lem  15218  limccnp2cntop  15219  limccoap  15220  dvrecap  15255  plyaddlem1  15289  plymullem1  15290  plycoeid3  15299  plyco  15301  plycj  15303  plyrecj  15305  dvply1  15307  dvply2g  15308  cosordlem  15391  logbgcd1irraplemexp  15510  logbgcd1irrap  15512  lgsneg1  15572  lgsdilem  15574  lgsdir2  15580  lgsdirprm  15581  lgsdir  15582  lgsne0  15585  lgsabs1  15586  lgsdirnn0  15594  lgsdinn0  15595  gausslemma2dlem1f1o  15607  gausslemma2dlem4  15611  lgseisenlem1  15617  lgsquadlem3  15626  2lgslem1a  15635  2sqlem5  15666  2sqlem7  15668  2sqlem8a  15669  2sqlem8  15670  2sqlem9  15671  gropeld  15718  grstructeld2dom  15719  uhgrm  15744  upgrm  15766  bj-stand  15818  bj-charfundcALT  15879  bj-charfunbi  15881  bj-bdfindis  16017  bj-peano4  16025  strcollnfALT  16056  1dom1el  16061  2omap  16067  pwtrufal  16069  pwf1oexmid  16071  subctctexmid  16072  pw1nct  16075  nnsf  16077  nninfalllem1  16080  nninfall  16081  nninfsellemqall  16087  nnnninfen  16093  exmidsbthrlem  16096  sbthom  16100  cvgcmp2nlemabs  16106  trilpo  16117  iswomni0  16125  redcwlpo  16129  dceqnconst  16134  dcapnconst  16135  nconstwlpolem  16139  nconstwlpo  16140  neapmkvlem  16141  neapmkv  16142  ltlenmkv  16144  taupi  16147  alsi1d  16155  alsi2d  16156  alsc1d  16157  alsc2d  16158