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  737  3mix3  1195  mpjao3dan  1344  ecase23d  1387  exlimdh  1645  nexd  1662  alexnim  1697  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  2424  eqnetrrid  2434  3netr3g  2437  necomd  2489  r19.21bi  2621  nrexdv  2626  rexlimd  2648  rabbidva  2791  elisset  2818  euind  2994  rmoan  3007  reuind  3012  2rmorex  3013  spsbc  3044  spesbc  3119  eldifad  3212  eldifbd  3213  3sstr3g  3270  sseqtrdi  3276  difindiss  3463  un00  3543  undifss  3577  ifcldcd  3647  disjpr2  3737  difprsn1  3817  diftpsn3  3819  difsnss  3824  sneqr  3848  preqr1  3856  preq12b  3858  oprcl  3891  intab  3962  riinm  4048  rintm  4068  disjiun  4088  sndisj  4089  3brtr3g  4126  trint  4207  iinexgm  4249  exmidexmid  4292  exmid01  4294  pwntru  4295  exmid1stab  4304  pwel  4316  exss  4325  0nelop  4346  euotd  4353  opelopabsb  4360  pwunim  4389  issod  4422  frind  4455  suctr  4524  orduniss  4528  onelini  4533  oneluni  4534  eusv2i  4558  rexxfrd  4566  rabxfrd  4572  reuhypd  4574  iunpw  4583  sucexg  4602  ordsucim  4604  ordtriexmidlem  4623  ontriexmidim  4626  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordsucunielexmid  4635  orddif  4651  suc11g  4661  onintexmid  4677  reg3exmidlemwe  4683  tfisi  4691  peano1  4698  peano2  4699  finds2  4705  omsinds  4726  brrelex12  4770  brel  4784  ssrel  4820  ssrel2  4822  ssrelrel  4832  elrel  4834  xpsspw  4844  relop  4886  dmxpm  4958  opelresi  5030  mptimass  5095  ndmima  5120  poirr2  5136  xpmlem  5164  xpimasn  5192  iotass  5311  iotacl  5318  dffun5r  5345  funeu  5358  funeu2  5359  funfnd  5364  funopg  5367  funun  5378  fununfun  5380  funinsn  5386  funtp  5390  funcnvuni  5406  funcnvres2  5412  imadiflem  5416  imadif  5417  funimaexglem  5420  fneu2  5444  fnimaeq0  5461  fnmpt  5466  fun2  5517  f00  5537  f0bi  5538  fimadmfo  5577  foimacnv  5610  resdif  5614  f1ococnv1  5621  fv3  5671  relelfvdm  5680  elfvm  5681  nfvres  5684  dffn5im  5700  mptfvex  5741  fvmptdf  5743  fvmptdv2  5745  fndmdif  5761  dff4im  5801  fmpt  5805  fmptd  5809  fmptdf  5812  f1oresrab  5820  fcoconst  5826  fsn  5827  funopsn  5838  ftpg  5846  fsnunf  5862  resfunexg  5883  isores1  5965  riota2df  6003  acexmidlemcase  6023  brabvv  6077  funoprabg  6130  fnovim  6140  ovmpodf  6163  ovi3  6169  elmpocl  6227  uchoice  6309  1stcof  6335  2ndcof  6336  opabn1stprc  6367  fnmpo  6376  fmpoco  6390  fo2ndf  6401  f1o2ndf1  6402  disjxp1  6410  fvdifsuppst  6422  fsuppeq  6425  fsuppeqg  6426  suppssrst  6439  suppssrgst  6440  brtpos2  6460  reldmtpos  6462  dftpos3  6471  dftpos4  6472  tpostpos2  6474  tposf2  6477  tposf12  6478  tposfo  6480  tposf  6481  smores2  6503  tfrlem1  6517  tfrlem3-2d  6521  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi1  6541  tfrexlem  6543  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcldm  6572  rdgivallem  6590  rdgisucinc  6594  frecabex  6607  frecfnom  6610  frecfcllem  6613  frecsuclem  6615  omsuc  6683  nntri2  6705  nnsucuniel  6706  nnsseleq  6712  nnm00  6741  ecexr  6750  swoer  6773  elqsn0m  6815  iinerm  6819  erinxp  6821  ecinxp  6822  eroveu  6838  eroprf  6840  mapprc  6864  mapsn  6902  ixpprc  6931  ixp0  6943  resixp  6945  elixpsn  6947  dom2lem  6988  fundmen  7024  1dom1el  7036  dom0  7067  xpf1o  7073  mapxpen  7077  xpmapenlem  7078  ssenen  7080  nneneq  7086  ssfilem  7105  ssfilemd  7107  dif1en  7111  dif1enen  7112  fin0  7117  fin0or  7118  diffitest  7119  diffisn  7125  ac6sfi  7130  fimax2gtrilemstep  7133  fimax2gtri  7134  finexdc  7135  eqsndc  7138  exmidpweq  7144  pw1fin  7145  onunsnss  7152  unsnfidcel  7156  undifdcss  7158  undifdc  7159  tpfidceq  7165  fiintim  7166  fisseneq  7170  fidcenumlemr  7197  sbthlemi4  7202  sbthlemi5  7203  sbthlemi9  7207  fifo  7222  suplubti  7242  supelti  7244  infmoti  7270  infisoti  7274  djulclb  7297  updjud  7324  omp1eomlem  7336  0ct  7349  ctmlemr  7350  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumct  7357  nninfninc  7365  nnnninfeq2  7371  finomni  7382  fodjuomnilemdc  7386  fodjum  7388  fodjuomnilemres  7390  fodjumkvlemres  7401  omniwomnimkv  7409  nninfwlporlem  7415  nninfwlpoimlemginf  7418  nninfwlpoim  7421  nninfinfwlpo  7422  ficardon  7436  pr2cv1  7443  exmidonfinlem  7447  en2eleq  7449  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  exmidfodomrlemim  7455  finacn  7462  acfun  7465  exmidaclem  7466  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  pw1if  7486  pw1on  7487  dftap2  7513  2omotaplemst  7520  exmidapne  7522  ccfunen  7526  cc1  7527  cc2lem  7528  cc2  7529  cc3  7530  acnccim  7534  elni2  7577  indpi  7605  distrnqg  7650  subhalfnqq  7677  enq0sym  7695  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nnnq0lem1  7709  distrnq0  7722  elinp  7737  elnp1st2nd  7739  prltlu  7750  prnmaxl  7751  prnminu  7752  prarloc  7766  nqprm  7805  appdivnq  7826  prmuloc  7829  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemdisj  7914  cauappcvgprlem2  7923  cauappcvgprlemlim  7924  caucvgprlemnkj  7929  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemdisj  7937  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem2  7943  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemlol  7961  caucvgprprlemexbt  7969  caucvgprprlem1  7972  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  prsrlem1  8005  gt0srpr  8011  caucvgsrlemcl  8052  caucvgsrlembound  8057  caucvgsrlemgt1  8058  suplocsrlemb  8069  suplocsrlem  8071  suplocsr  8072  ltresr  8102  nnindnn  8156  axcaucvglemcl  8158  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  sup3exmid  9179  nnind  9201  nn0supp  9498  nn0ge2m1nn  9506  zleloe  9570  zapne  9598  nn0lt2  9605  suprzclex  9622  zindd  9642  uzm1  9831  uzin  9833  infregelbex  9876  elnn1uz2  9885  nn01to3  9895  divfnzn  9899  qapne  9917  xrltnsym2  10073  xaddass  10148  xleadd1a  10152  xlt2add  10159  xlesubadd  10162  iooval2  10194  icoshftf1o  10270  fztri3or  10319  fzneuz  10381  4fvwrd4  10420  elfzo0  10466  infssuzex  10539  infssuzcldc  10541  suprzubdc  10542  nninfdcex  10543  zsupssdc  10544  exbtwnzlemex  10555  ioom  10566  fzfig  10738  uzennn  10744  uzsinds  10752  iseqovex  10766  seq3val  10768  seqvalcd  10769  seqf  10772  seqovcd  10775  monoord2  10794  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seq3f1olemqsum  10821  seq3f1o  10825  seqf1og  10829  seq3distr  10840  expp1  10854  expcl2lemap  10859  expclzap  10872  expap0i  10879  nn0ltexp2  11017  bcval5  11071  hashinfuni  11085  hashennnuni  11087  hashnncl  11103  resunimafz0  11141  zfz1isolemiso  11149  zfz1isolem1  11150  zfz1iso  11151  wrdsymb0  11195  wrdlen1  11200  ccat1st1st  11267  swrdrlen  11291  pfxid  11316  pfxwrdsymbg  11320  pfxtrcfv  11323  pfxccat1  11332  pfxpfxid  11339  pfxcctswrd  11340  swrdccatin1  11355  pfxccatin12  11363  pfxccatid  11371  seq3shft  11461  cvg1nlemcau  11607  rexanuz  11611  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  rersqreu  11651  caubnd2  11740  maxleast  11836  fimaxre2  11850  minmax  11853  xrmaxiflemcl  11868  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxadd  11884  xrminmax  11888  xrbdtri  11899  climreu  11920  reccn2ap  11936  iserex  11962  climcvg1nlem  11972  serf0  11975  fz1f1o  11998  summodclem3  12004  zsumdc  12008  fsum3  12011  isumz  12013  isumss  12015  isumss2  12017  fsumsersdc  12019  fsum3ser  12021  fsumsplit  12031  isumclim2  12046  isumclim3  12047  fsum2dlemstep  12058  fsumcnv  12061  fisumcom2  12062  bcxmas  12113  isumle  12119  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratz  12156  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  zproddc  12203  prod1dc  12210  fprodsplitdc  12220  fprodsplit  12221  fprodunsn  12228  fprodcl2lem  12229  fprodcllemf  12237  fprod2dlemstep  12246  fprodcnv  12249  fprodcom2fi  12250  fprodle  12264  ef0lem  12284  fsumdvds  12466  mod2eq1n2dvds  12503  ndvdssub  12554  bitsfzolem  12578  bitsfzo  12579  bitsinv1  12586  gcdsupex  12591  gcdsupcl  12592  bezoutlemnewy  12630  bezoutlemmain  12632  bezoutlembi  12639  bezoutlemeu  12641  bezoutlemle  12642  uzwodc  12671  nnwofdc  12672  nnwosdc  12673  nninfctlemfo  12674  nninfct  12675  nn0seqcvgd  12676  eucalgf  12690  eucalginv  12691  lcmval  12698  prmind2  12755  dfphi2  12855  phiprmpw  12857  phimullem  12860  eulerthlem1  12862  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  eulerth  12868  phisum  12876  odzcllem  12878  odzdvds  12881  pythagtriplem19  12918  pclemub  12923  pcprecl  12925  pceu  12931  pcqmul  12939  pcqcl  12942  pcxnn0cl  12946  pcxqcl  12948  pcge0  12949  pcdvdsb  12956  pceq0  12958  pcneg  12961  pcdvdstr  12963  pcgcd1  12964  pc2dvds  12966  pcz  12968  pcprmpw2  12969  pcaddlem  12975  pcadd  12976  pcmptcl  12978  pcmpt  12979  pcmptdvds  12981  fldivp1  12984  qexpz  12988  pockthlem  12992  pockthg  12993  prmunb  12998  1arith  13003  4sqlemffi  13032  4sqlem17  13043  4sqlem18  13044  4sqlem19  13045  ennnfonelemom  13092  ennnfoneleminc  13095  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemdm  13104  ennnfonelemr  13107  ennnfonelemim  13108  exmidunben  13110  ctinfom  13112  inffinp1  13113  ctinf  13114  enctlem  13116  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  ctiunctlemudc  13121  ctiunct  13124  ctiunctal  13125  unct  13126  ssomct  13129  nninfdclemcl  13132  nninfdclemp1  13134  nninfdc  13137  structcnvcnv  13161  setscom  13185  relelbasov  13208  ressbas2d  13214  ressval3d  13218  ressabsg  13222  restid2  13394  imasaddfnlemg  13460  quslem  13470  ercpbl  13477  fnpr2ob  13486  mgmplusf  13512  grpinvalem  13531  grpinva  13532  grprida  13533  fngsum  13534  igsumvalx  13535  gsum0g  13542  gsumval2  13543  ismnd  13565  mhmpropd  13612  grppropd  13663  grpsubf  13725  dfgrp3mlem  13744  mulgnn0p1  13783  mulgnn0subcl  13785  mulgsubcl  13786  mulgneg  13790  mulgnn0dir  13802  mulgnn0ass  13808  submmulg  13816  issubg2m  13839  issubg4m  13843  ghmmulg  13906  ghmrn  13907  lringuplu  14274  rrgsupp  14344  lmodscaf  14389  lssintclm  14463  lspun0  14504  lidlbas  14557  psrbagconcl  14756  psr1clfi  14772  topontopon  14814  eltg3i  14850  epttop  14884  difopn  14902  uncld  14907  0nnei  14947  resttopon  14965  restabs  14969  restopnb  14975  lmcvg  15011  cnptopco  15016  cnss1  15020  cnss2  15021  cncnpi  15022  cncnp2m  15025  cnrest  15029  cnrest2  15030  cnrest2r  15031  cnptoprest  15033  cnptoprest2  15034  lmss  15040  lmff  15043  lmtopcnp  15044  lmcn  15045  txbasval  15061  upxp  15066  txcnmpt  15067  txdis1cn  15072  txlm  15073  lmcn2  15074  cnmpt11  15077  cnmpt11f  15078  cnmpt1t  15079  cnmpt12  15081  cnmpt21  15085  cnmpt21f  15086  cnmpt2t  15087  cnmpt22  15088  cnmpt22f  15089  cnmptcom  15092  hmeocnv  15101  hmeof1o  15103  hmeores  15109  txhmeo  15113  txswaphmeo  15115  isxmet2d  15142  blfvalps  15179  xblss2ps  15198  xblss2  15199  blfps  15203  blf  15204  unirnblps  15216  unirnbl  15217  isxms2  15246  bdxmet  15295  bdmet  15296  xmetxp  15301  xmettx  15304  blssioo  15347  tgioo  15348  mulcncflem  15401  divcncfap  15408  dedekindeulemuub  15411  dedekindeulemub  15412  dedekindeulemloc  15413  dedekindeulemlu  15415  suplociccreex  15418  suplociccex  15419  dedekindicclemuub  15420  dedekindicclemub  15421  dedekindicclemloc  15422  dedekindicclemlu  15424  dedekindicc  15427  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthdich  15447  limcrcl  15452  limcmpted  15457  limccnp2lem  15470  limccnp2cntop  15471  limccoap  15472  dvrecap  15507  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  plyco  15553  plycj  15555  plyrecj  15557  dvply1  15559  dvply2g  15560  cosordlem  15643  logbgcd1irraplemexp  15762  logbgcd1irrap  15764  lgsneg1  15827  lgsdilem  15829  lgsdir2  15835  lgsdirprm  15836  lgsdir  15837  lgsne0  15840  lgsabs1  15841  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1f1o  15862  gausslemma2dlem4  15866  lgseisenlem1  15872  lgsquadlem3  15881  2lgslem1a  15890  2sqlem5  15921  2sqlem7  15923  2sqlem8a  15924  2sqlem8  15925  2sqlem9  15926  gropeld  15973  grstructeld2dom  15974  uhgrm  16002  upgrm  16024  upgr1een  16048  uhgredgm  16060  edgupgren  16065  edgumgren  16066  edgusgren  16087  ausgrusgrben  16092  umgr2edg1  16133  usgredg2vlem1  16146  uhgr0enedgfi  16160  subupgr  16197  vtxedgfi  16213  vtxlpfi  16214  vtxdumgrfival  16222  vtxd0nedgbfi  16223  1hevtxdg0fi  16231  p1evtxdeqfilem  16235  wlkvtxm  16264  g0wlk0  16294  wlkres  16303  trlreslem  16313  clwwlkccatlem  16324  clwwlknnn  16336  trlsegvdeglem6  16389  eupth2lem3lem3fi  16394  eupth2lem3lem7fi  16398  eulerpathum  16405  bj-stand  16449  bj-charfundcALT  16508  bj-charfunbi  16510  bj-bdfindis  16646  bj-peano4  16654  strcollnfALT  16685  2omap  16698  pw1map  16700  pwtrufal  16702  pwf1oexmid  16704  subctctexmid  16705  pw1nct  16708  nnsf  16714  nninfalllem1  16717  nninfall  16718  nninfsellemqall  16724  nnnninfen  16730  exmidsbthrlem  16733  sbthom  16737  repiecef  16743  cvgcmp2nlemabs  16747  trilpo  16758  iswomni0  16767  redcwlpo  16771  dceqnconst  16776  dcapnconst  16777  nconstwlpolem  16781  nconstwlpo  16782  neapmkvlem  16783  neapmkv  16784  ltlenmkv  16786  taupi  16789  gfsumval  16792  gsumgfsum  16796  alsi1d  16807  alsi2d  16808  alsc1d  16809  alsc2d  16810