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  736  3mix3  1194  mpjao3dan  1343  ecase23d  1386  exlimdh  1644  nexd  1661  alexnim  1696  excomim  1711  19.41  1734  equcomd  1755  nfexd  1809  sbh  1824  sbcof2  1858  sbidm  1899  sb6rf  1901  nfsbt  2029  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  eu2  2124  2euex  2167  eqcomd  2237  3eltr3g  2316  abbid  2348  neneqd  2423  eqnetrrid  2433  3netr3g  2436  necomd  2488  r19.21bi  2620  nrexdv  2625  rexlimd  2647  rabbidva  2790  elisset  2817  euind  2993  rmoan  3006  reuind  3011  2rmorex  3012  spsbc  3043  spesbc  3118  eldifad  3211  eldifbd  3212  3sstr3g  3269  sseqtrdi  3275  difindiss  3461  un00  3541  undifss  3575  ifcldcd  3643  disjpr2  3733  difprsn1  3812  diftpsn3  3814  difsnss  3819  sneqr  3843  preqr1  3851  preq12b  3853  oprcl  3886  intab  3957  riinm  4043  rintm  4063  disjiun  4083  sndisj  4084  3brtr3g  4121  trint  4202  iinexgm  4244  exmidexmid  4286  exmid01  4288  pwntru  4289  exmid1stab  4298  pwel  4310  exss  4319  0nelop  4340  euotd  4347  opelopabsb  4354  pwunim  4383  issod  4416  frind  4449  suctr  4518  orduniss  4522  onelini  4527  oneluni  4528  eusv2i  4552  rexxfrd  4560  rabxfrd  4566  reuhypd  4568  iunpw  4577  sucexg  4596  ordsucim  4598  ordtriexmidlem  4617  ontriexmidim  4620  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordsucunielexmid  4629  orddif  4645  suc11g  4655  onintexmid  4671  reg3exmidlemwe  4677  tfisi  4685  peano1  4692  peano2  4693  finds2  4699  omsinds  4720  brrelex12  4764  brel  4778  ssrel  4814  ssrel2  4816  ssrelrel  4826  elrel  4828  xpsspw  4838  relop  4880  dmxpm  4952  opelresi  5024  mptimass  5089  ndmima  5113  poirr2  5129  xpmlem  5157  xpimasn  5185  iotass  5304  iotacl  5311  dffun5r  5338  funeu  5351  funeu2  5352  funfnd  5357  funopg  5360  funun  5371  fununfun  5373  funinsn  5379  funtp  5383  funcnvuni  5399  funcnvres2  5405  imadiflem  5409  imadif  5410  funimaexglem  5413  fneu2  5437  fnimaeq0  5454  fnmpt  5459  fun2  5509  f00  5528  f0bi  5529  fimadmfo  5568  foimacnv  5601  resdif  5605  f1ococnv1  5612  fv3  5662  relelfvdm  5671  elfvm  5672  nfvres  5675  dffn5im  5691  mptfvex  5732  fvmptdf  5734  fvmptdv2  5736  fndmdif  5752  dff4im  5793  fmpt  5797  fmptd  5801  fmptdf  5804  f1oresrab  5812  fcoconst  5818  fsn  5819  funopsn  5829  ftpg  5837  fsnunf  5853  resfunexg  5874  isores1  5954  riota2df  5992  acexmidlemcase  6012  brabvv  6066  funoprabg  6119  fnovim  6129  ovmpodf  6152  ovi3  6158  elmpocl  6216  uchoice  6299  1stcof  6325  2ndcof  6326  opabn1stprc  6357  fnmpo  6366  fmpoco  6380  fo2ndf  6391  f1o2ndf1  6392  disjxp1  6400  brtpos2  6416  reldmtpos  6418  dftpos3  6427  dftpos4  6428  tpostpos2  6430  tposf2  6433  tposf12  6434  tposfo  6436  tposf  6437  smores2  6459  tfrlem1  6473  tfrlem3-2d  6477  tfrlemisucaccv  6490  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrlemi1  6497  tfrexlem  6499  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcldm  6528  rdgivallem  6546  rdgisucinc  6550  frecabex  6563  frecfnom  6566  frecfcllem  6569  frecsuclem  6571  omsuc  6639  nntri2  6661  nnsucuniel  6662  nnsseleq  6668  nnm00  6697  ecexr  6706  swoer  6729  elqsn0m  6771  iinerm  6775  erinxp  6777  ecinxp  6778  eroveu  6794  eroprf  6796  mapprc  6820  mapsn  6858  ixpprc  6887  ixp0  6899  resixp  6901  elixpsn  6903  dom2lem  6944  fundmen  6980  1dom1el  6992  dom0  7023  xpf1o  7029  mapxpen  7033  xpmapenlem  7034  ssenen  7036  nneneq  7042  ssfilem  7061  ssfilemd  7063  dif1en  7067  dif1enen  7068  fin0  7073  fin0or  7074  diffitest  7075  diffisn  7081  ac6sfi  7086  fimax2gtrilemstep  7089  fimax2gtri  7090  finexdc  7091  eqsndc  7094  exmidpweq  7100  pw1fin  7101  onunsnss  7108  unsnfidcel  7112  undifdcss  7114  undifdc  7115  tpfidceq  7121  fiintim  7122  fisseneq  7126  fidcenumlemr  7153  sbthlemi4  7158  sbthlemi5  7159  sbthlemi9  7163  fifo  7178  suplubti  7198  supelti  7200  infmoti  7226  infisoti  7230  djulclb  7253  updjud  7280  omp1eomlem  7292  0ct  7305  ctmlemr  7306  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumct  7313  nninfninc  7321  nnnninfeq2  7327  finomni  7338  fodjuomnilemdc  7342  fodjum  7344  fodjuomnilemres  7346  fodjumkvlemres  7357  omniwomnimkv  7365  nninfwlporlem  7371  nninfwlpoimlemginf  7374  nninfwlpoim  7377  nninfinfwlpo  7378  ficardon  7392  pr2cv1  7399  exmidonfinlem  7403  en2eleq  7405  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  exmidfodomrlemim  7411  finacn  7418  acfun  7421  exmidaclem  7422  exmidontriimlem3  7437  exmidontriimlem4  7438  exmidontriim  7439  pw1if  7442  pw1on  7443  dftap2  7469  2omotaplemst  7476  exmidapne  7478  ccfunen  7482  cc1  7483  cc2lem  7484  cc2  7485  cc3  7486  acnccim  7490  elni2  7533  indpi  7561  distrnqg  7606  subhalfnqq  7633  enq0sym  7651  enq0ref  7652  enq0tr  7653  nqnq0pi  7657  nnnq0lem1  7665  distrnq0  7678  elinp  7693  elnp1st2nd  7695  prltlu  7706  prnmaxl  7707  prnminu  7708  prarloc  7722  nqprm  7761  appdivnq  7782  prmuloc  7785  mullocpr  7790  distrlem4prl  7803  distrlem4pru  7804  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  cauappcvgprlemopl  7865  cauappcvgprlemopu  7867  cauappcvgprlemdisj  7870  cauappcvgprlem2  7879  cauappcvgprlemlim  7880  caucvgprlemnkj  7885  caucvgprlemopl  7888  caucvgprlemopu  7890  caucvgprlemdisj  7893  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem2  7899  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemlol  7917  caucvgprprlemexbt  7925  caucvgprprlem1  7928  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  prsrlem1  7961  gt0srpr  7967  caucvgsrlemcl  8008  caucvgsrlembound  8013  caucvgsrlemgt1  8014  suplocsrlemb  8025  suplocsrlem  8027  suplocsr  8028  ltresr  8058  nnindnn  8112  axcaucvglemcl  8114  axcaucvglemval  8116  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  sup3exmid  9136  nnind  9158  nn0supp  9453  nn0ge2m1nn  9461  zleloe  9525  zapne  9553  nn0lt2  9560  suprzclex  9577  zindd  9597  uzm1  9786  uzin  9788  infregelbex  9831  elnn1uz2  9840  nn01to3  9850  divfnzn  9854  qapne  9872  xrltnsym2  10028  xaddass  10103  xleadd1a  10107  xlt2add  10114  xlesubadd  10117  iooval2  10149  icoshftf1o  10225  fztri3or  10273  fzneuz  10335  4fvwrd4  10374  elfzo0  10420  infssuzex  10492  infssuzcldc  10494  suprzubdc  10495  nninfdcex  10496  zsupssdc  10497  exbtwnzlemex  10508  ioom  10519  fzfig  10691  uzennn  10697  uzsinds  10705  iseqovex  10719  seq3val  10721  seqvalcd  10722  seqf  10725  seqovcd  10728  monoord2  10747  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seq3f1olemqsum  10774  seq3f1o  10778  seqf1og  10782  seq3distr  10793  expp1  10807  expcl2lemap  10812  expclzap  10825  expap0i  10832  nn0ltexp2  10970  bcval5  11024  hashinfuni  11038  hashennnuni  11040  hashnncl  11056  resunimafz0  11094  zfz1isolemiso  11102  zfz1isolem1  11103  zfz1iso  11104  wrdsymb0  11145  wrdlen1  11150  ccat1st1st  11217  swrdrlen  11241  pfxid  11266  pfxwrdsymbg  11270  pfxtrcfv  11273  pfxccat1  11282  pfxpfxid  11289  pfxcctswrd  11290  swrdccatin1  11305  pfxccatin12  11313  pfxccatid  11321  seq3shft  11398  cvg1nlemcau  11544  rexanuz  11548  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  rersqreu  11588  caubnd2  11677  maxleast  11773  fimaxre2  11787  minmax  11790  xrmaxiflemcl  11805  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxadd  11821  xrminmax  11825  xrbdtri  11836  climreu  11857  reccn2ap  11873  iserex  11899  climcvg1nlem  11909  serf0  11912  fz1f1o  11935  summodclem3  11940  zsumdc  11944  fsum3  11947  isumz  11949  isumss  11951  isumss2  11953  fsumsersdc  11955  fsum3ser  11957  fsumsplit  11967  isumclim2  11982  isumclim3  11983  fsum2dlemstep  11994  fsumcnv  11997  fisumcom2  11998  bcxmas  12049  isumle  12055  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratz  12092  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  zproddc  12139  prod1dc  12146  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  fprodcl2lem  12165  fprodcllemf  12173  fprod2dlemstep  12182  fprodcnv  12185  fprodcom2fi  12186  fprodle  12200  ef0lem  12220  fsumdvds  12402  mod2eq1n2dvds  12439  ndvdssub  12490  bitsfzolem  12514  bitsfzo  12515  bitsinv1  12522  gcdsupex  12527  gcdsupcl  12528  bezoutlemnewy  12566  bezoutlemmain  12568  bezoutlembi  12575  bezoutlemeu  12577  bezoutlemle  12578  uzwodc  12607  nnwofdc  12608  nnwosdc  12609  nninfctlemfo  12610  nninfct  12611  nn0seqcvgd  12612  eucalgf  12626  eucalginv  12627  lcmval  12634  prmind2  12691  dfphi2  12791  phiprmpw  12793  phimullem  12796  eulerthlem1  12798  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  eulerth  12804  phisum  12812  odzcllem  12814  odzdvds  12817  pythagtriplem19  12854  pclemub  12859  pcprecl  12861  pceu  12867  pcqmul  12875  pcqcl  12878  pcxnn0cl  12882  pcxqcl  12884  pcge0  12885  pcdvdsb  12892  pceq0  12894  pcneg  12897  pcdvdstr  12899  pcgcd1  12900  pc2dvds  12902  pcz  12904  pcprmpw2  12905  pcaddlem  12911  pcadd  12912  pcmptcl  12914  pcmpt  12915  pcmptdvds  12917  fldivp1  12920  qexpz  12924  pockthlem  12928  pockthg  12929  prmunb  12934  1arith  12939  4sqlemffi  12968  4sqlem17  12979  4sqlem18  12980  4sqlem19  12981  ennnfonelemom  13028  ennnfoneleminc  13031  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemdm  13040  ennnfonelemr  13043  ennnfonelemim  13044  exmidunben  13046  ctinfom  13048  inffinp1  13049  ctinf  13050  enctlem  13052  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  ctiunctlemudc  13057  ctiunct  13060  ctiunctal  13061  unct  13062  ssomct  13065  nninfdclemcl  13068  nninfdclemp1  13070  nninfdc  13073  structcnvcnv  13097  setscom  13121  relelbasov  13144  ressbas2d  13150  ressval3d  13154  ressabsg  13158  restid2  13330  imasaddfnlemg  13396  quslem  13406  ercpbl  13413  fnpr2ob  13422  mgmplusf  13448  grpinvalem  13467  grpinva  13468  grprida  13469  fngsum  13470  igsumvalx  13471  gsum0g  13478  gsumval2  13479  ismnd  13501  mhmpropd  13548  grppropd  13599  grpsubf  13661  dfgrp3mlem  13680  mulgnn0p1  13719  mulgnn0subcl  13721  mulgsubcl  13722  mulgneg  13726  mulgnn0dir  13738  mulgnn0ass  13744  submmulg  13752  issubg2m  13775  issubg4m  13779  ghmmulg  13842  ghmrn  13843  lringuplu  14209  lmodscaf  14323  lssintclm  14397  lspun0  14438  lidlbas  14491  psr1clfi  14701  topontopon  14743  eltg3i  14779  epttop  14813  difopn  14831  uncld  14836  0nnei  14876  resttopon  14894  restabs  14898  restopnb  14904  lmcvg  14940  cnptopco  14945  cnss1  14949  cnss2  14950  cncnpi  14951  cncnp2m  14954  cnrest  14958  cnrest2  14959  cnrest2r  14960  cnptoprest  14962  cnptoprest2  14963  lmss  14969  lmff  14972  lmtopcnp  14973  lmcn  14974  txbasval  14990  upxp  14995  txcnmpt  14996  txdis1cn  15001  txlm  15002  lmcn2  15003  cnmpt11  15006  cnmpt11f  15007  cnmpt1t  15008  cnmpt12  15010  cnmpt21  15014  cnmpt21f  15015  cnmpt2t  15016  cnmpt22  15017  cnmpt22f  15018  cnmptcom  15021  hmeocnv  15030  hmeof1o  15032  hmeores  15038  txhmeo  15042  txswaphmeo  15044  isxmet2d  15071  blfvalps  15108  xblss2ps  15127  xblss2  15128  blfps  15132  blf  15133  unirnblps  15145  unirnbl  15146  isxms2  15175  bdxmet  15224  bdmet  15225  xmetxp  15230  xmettx  15233  blssioo  15276  tgioo  15277  mulcncflem  15330  divcncfap  15337  dedekindeulemuub  15340  dedekindeulemub  15341  dedekindeulemloc  15342  dedekindeulemlu  15344  suplociccreex  15347  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemub  15350  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthdich  15376  limcrcl  15381  limcmpted  15386  limccnp2lem  15399  limccnp2cntop  15400  limccoap  15401  dvrecap  15436  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plyco  15482  plycj  15484  plyrecj  15486  dvply1  15488  dvply2g  15489  cosordlem  15572  logbgcd1irraplemexp  15691  logbgcd1irrap  15693  lgsneg1  15753  lgsdilem  15755  lgsdir2  15761  lgsdirprm  15762  lgsdir  15763  lgsne0  15766  lgsabs1  15767  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1f1o  15788  gausslemma2dlem4  15792  lgseisenlem1  15798  lgsquadlem3  15807  2lgslem1a  15816  2sqlem5  15847  2sqlem7  15849  2sqlem8a  15850  2sqlem8  15851  2sqlem9  15852  gropeld  15899  grstructeld2dom  15900  uhgrm  15928  upgrm  15950  upgr1een  15974  uhgredgm  15986  edgupgren  15991  edgumgren  15992  edgusgren  16013  ausgrusgrben  16018  umgr2edg1  16059  usgredg2vlem1  16072  uhgr0enedgfi  16086  subupgr  16123  vtxedgfi  16139  vtxlpfi  16140  vtxdumgrfival  16148  vtxd0nedgbfi  16149  1hevtxdg0fi  16157  p1evtxdeqfilem  16161  wlkvtxm  16190  g0wlk0  16220  wlkres  16229  trlreslem  16239  clwwlkccatlem  16250  clwwlknnn  16262  trlsegvdeglem6  16315  bj-stand  16344  bj-charfundcALT  16404  bj-charfunbi  16406  bj-bdfindis  16542  bj-peano4  16550  strcollnfALT  16581  2omap  16594  pw1map  16596  pwtrufal  16598  pwf1oexmid  16600  subctctexmid  16601  pw1nct  16604  nnsf  16607  nninfalllem1  16610  nninfall  16611  nninfsellemqall  16617  nnnninfen  16623  exmidsbthrlem  16626  sbthom  16630  cvgcmp2nlemabs  16636  trilpo  16647  iswomni0  16655  redcwlpo  16659  dceqnconst  16664  dcapnconst  16665  nconstwlpolem  16669  nconstwlpo  16670  neapmkvlem  16671  neapmkv  16672  ltlenmkv  16674  taupi  16677  gfsumval  16680  gsumgfsum  16684  alsi1d  16692  alsi2d  16693  alsc1d  16694  alsc2d  16695