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  729  3mix3  1168  mpjao3dan  1307  ecase23d  1350  exlimdh  1596  nexd  1613  alexnim  1648  excomim  1663  19.41  1686  equcomd  1707  nfexd  1761  sbh  1776  sbcof2  1810  sbidm  1851  sb6rf  1853  nfsbt  1976  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eu2  2070  2euex  2113  eqcomd  2183  3eltr3g  2262  abbid  2294  neneqd  2368  eqnetrrid  2378  3netr3g  2381  necomd  2433  r19.21bi  2565  nrexdv  2570  rexlimd  2591  rabbidva  2725  elisset  2751  euind  2924  rmoan  2937  reuind  2942  2rmorex  2943  spsbc  2974  spesbc  3048  eldifad  3140  eldifbd  3141  3sstr3g  3197  sseqtrdi  3203  difindiss  3389  un00  3469  undifss  3503  ifcldcd  3570  disjpr2  3656  difprsn1  3731  diftpsn3  3733  difsnss  3738  sneqr  3760  preqr1  3768  preq12b  3770  oprcl  3802  intab  3873  riinm  3959  rintm  3979  disjiun  3998  sndisj  3999  3brtr3g  4036  trint  4116  iinexgm  4154  exmidexmid  4196  exmid01  4198  pwntru  4199  exmid1stab  4208  pwel  4218  exss  4227  0nelop  4248  euotd  4254  opelopabsb  4260  pwunim  4286  issod  4319  frind  4352  suctr  4421  orduniss  4425  onelini  4430  oneluni  4431  eusv2i  4455  rexxfrd  4463  rabxfrd  4469  reuhypd  4471  iunpw  4480  sucexg  4497  ordsucim  4499  ordtriexmidlem  4518  ontriexmidim  4521  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  ordsucunielexmid  4530  orddif  4546  suc11g  4556  onintexmid  4572  reg3exmidlemwe  4578  tfisi  4586  peano1  4593  peano2  4594  finds2  4600  omsinds  4621  brrelex12  4664  brel  4678  ssrel  4714  ssrel2  4716  ssrelrel  4726  elrel  4728  xpsspw  4738  relop  4777  dmxpm  4847  opelresi  4918  ndmima  5005  poirr2  5021  xpmlem  5049  xpimasn  5077  iotass  5195  iotacl  5201  dffun5r  5228  funeu  5241  funeu2  5242  funfnd  5247  funopg  5250  funun  5260  funinsn  5265  funtp  5269  funcnvuni  5285  funcnvres2  5291  imadiflem  5295  imadif  5296  funimaexglem  5299  fneu2  5321  fnimaeq0  5337  fnmpt  5342  fun2  5389  f00  5407  f0bi  5408  foimacnv  5479  resdif  5483  f1ococnv1  5490  fv3  5538  relelfvdm  5547  nfvres  5548  dffn5im  5561  mptfvex  5601  fvmptdf  5603  fvmptdv2  5605  fndmdif  5621  dff4im  5662  fmpt  5666  fmptd  5670  fmptdf  5673  f1oresrab  5681  fcoconst  5687  fsn  5688  ftpg  5700  fsnunf  5716  resfunexg  5737  isores1  5814  riota2df  5850  acexmidlemcase  5869  brabvv  5920  funoprabg  5973  fnovim  5982  ovmpodf  6005  ovi3  6010  elmpocl  6068  1stcof  6163  2ndcof  6164  fnmpo  6202  fmpoco  6216  fo2ndf  6227  f1o2ndf1  6228  disjxp1  6236  brtpos2  6251  reldmtpos  6253  dftpos3  6262  dftpos4  6263  tpostpos2  6265  tposf2  6268  tposf12  6269  tposfo  6271  tposf  6272  smores2  6294  tfrlem1  6308  tfrlem3-2d  6312  tfrlemisucaccv  6325  tfrlemibxssdm  6327  tfrlemibfn  6328  tfrlemi1  6332  tfrexlem  6334  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemaccex  6361  tfrcldm  6363  rdgivallem  6381  rdgisucinc  6385  frecabex  6398  frecfnom  6401  frecfcllem  6404  frecsuclem  6406  omsuc  6472  nntri2  6494  nnsucuniel  6495  nnsseleq  6501  nnm00  6530  ecexr  6539  swoer  6562  elqsn0m  6602  iinerm  6606  erinxp  6608  ecinxp  6609  eroveu  6625  eroprf  6627  mapprc  6651  mapsn  6689  ixpprc  6718  ixp0  6730  resixp  6732  elixpsn  6734  dom2lem  6771  fundmen  6805  dom0  6837  xpf1o  6843  mapxpen  6847  xpmapenlem  6848  ssenen  6850  nneneq  6856  ssfilem  6874  dif1en  6878  dif1enen  6879  fin0  6884  fin0or  6885  diffitest  6886  diffisn  6892  ac6sfi  6897  fimax2gtrilemstep  6899  fimax2gtri  6900  finexdc  6901  exmidpweq  6908  pw1fin  6909  onunsnss  6915  unsnfidcel  6919  undifdcss  6921  undifdc  6922  fiintim  6927  fisseneq  6930  fidcenumlemr  6953  sbthlemi4  6958  sbthlemi5  6959  sbthlemi9  6963  fifo  6978  suplubti  6998  supelti  7000  infmoti  7026  infisoti  7030  djulclb  7053  updjud  7080  omp1eomlem  7092  0ct  7105  ctmlemr  7106  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  enumct  7113  nnnninfeq2  7126  finomni  7137  fodjuomnilemdc  7141  fodjum  7143  fodjuomnilemres  7145  fodjumkvlemres  7156  omniwomnimkv  7164  nninfwlporlem  7170  nninfwlpoimlemginf  7173  nninfwlpoim  7175  exmidonfinlem  7191  en2eleq  7193  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  exmidfodomrlemim  7199  acfun  7205  exmidaclem  7206  exmidontriimlem3  7221  exmidontriimlem4  7222  exmidontriim  7223  pw1on  7224  dftap2  7249  2omotaplemst  7256  exmidapne  7258  ccfunen  7262  cc1  7263  cc2lem  7264  cc2  7265  cc3  7266  elni2  7312  indpi  7340  distrnqg  7385  subhalfnqq  7412  enq0sym  7430  enq0ref  7431  enq0tr  7432  nqnq0pi  7436  nnnq0lem1  7444  distrnq0  7457  elinp  7472  elnp1st2nd  7474  prltlu  7485  prnmaxl  7486  prnminu  7487  prarloc  7501  nqprm  7540  appdivnq  7561  prmuloc  7564  mullocpr  7569  distrlem4prl  7582  distrlem4pru  7583  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  cauappcvgprlemopl  7644  cauappcvgprlemopu  7646  cauappcvgprlemdisj  7649  cauappcvgprlem2  7658  cauappcvgprlemlim  7659  caucvgprlemnkj  7664  caucvgprlemopl  7667  caucvgprlemopu  7669  caucvgprlemdisj  7672  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem2  7678  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemlol  7696  caucvgprprlemexbt  7704  caucvgprprlem1  7707  suplocexprlemrl  7715  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  suplocexprlemlub  7722  prsrlem1  7740  gt0srpr  7746  caucvgsrlemcl  7787  caucvgsrlembound  7792  caucvgsrlemgt1  7793  suplocsrlemb  7804  suplocsrlem  7806  suplocsr  7807  ltresr  7837  nnindnn  7891  axcaucvglemcl  7893  axcaucvglemval  7895  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  axpre-suploc  7900  sup3exmid  8913  nnind  8934  nn0supp  9227  nn0ge2m1nn  9235  zleloe  9299  zapne  9326  nn0lt2  9333  suprzclex  9350  zindd  9370  uzm1  9557  uzin  9559  infregelbex  9597  elnn1uz2  9606  nn01to3  9616  divfnzn  9620  qapne  9638  xrltnsym2  9793  xaddass  9868  xleadd1a  9872  xlt2add  9879  xlesubadd  9882  iooval2  9914  icoshftf1o  9990  fztri3or  10038  fzneuz  10100  4fvwrd4  10139  elfzo0  10181  exbtwnzlemex  10249  ioom  10260  fzfig  10429  uzennn  10435  uzsinds  10441  iseqovex  10455  seq3val  10457  seqvalcd  10458  seqf  10460  seqovcd  10462  monoord2  10476  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  seq3f1olemqsum  10499  seq3f1o  10503  seq3distr  10512  expp1  10526  expcl2lemap  10531  expclzap  10544  expap0i  10551  nn0ltexp2  10688  bcval5  10742  hashinfuni  10756  hashennnuni  10758  hashnncl  10774  resunimafz0  10810  zfz1isolemiso  10818  zfz1isolem1  10819  zfz1iso  10820  seq3shft  10846  cvg1nlemcau  10992  rexanuz  10996  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemsqa  11032  resqrexlemex  11033  rersqreu  11036  caubnd2  11125  maxleast  11221  fimaxre2  11234  minmax  11237  xrmaxiflemcl  11252  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxadd  11268  xrminmax  11272  xrbdtri  11283  climreu  11304  reccn2ap  11320  iserex  11346  climcvg1nlem  11356  serf0  11359  fz1f1o  11382  summodclem3  11387  zsumdc  11391  fsum3  11394  isumz  11396  isumss  11398  isumss2  11400  fsumsersdc  11402  fsum3ser  11404  fsumsplit  11414  isumclim2  11429  isumclim3  11430  fsum2dlemstep  11441  fsumcnv  11444  fisumcom2  11445  bcxmas  11496  isumle  11502  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratz  11539  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  zproddc  11586  prod1dc  11593  fprodsplitdc  11603  fprodsplit  11604  fprodunsn  11611  fprodcl2lem  11612  fprodcllemf  11620  fprod2dlemstep  11629  fprodcnv  11632  fprodcom2fi  11633  fprodle  11647  ef0lem  11667  mod2eq1n2dvds  11883  ndvdssub  11934  infssuzex  11949  infssuzcldc  11951  suprzubdc  11952  nninfdcex  11953  zsupssdc  11954  gcdsupex  11957  gcdsupcl  11958  bezoutlemnewy  11996  bezoutlemmain  11998  bezoutlembi  12005  bezoutlemeu  12007  bezoutlemle  12008  uzwodc  12037  nnwofdc  12038  nnwosdc  12039  nn0seqcvgd  12040  eucalgf  12054  eucalginv  12055  lcmval  12062  prmind2  12119  dfphi2  12219  phiprmpw  12221  phimullem  12224  eulerthlem1  12226  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  eulerth  12232  phisum  12239  odzcllem  12241  odzdvds  12244  pythagtriplem19  12281  pclemub  12286  pcprecl  12288  pceu  12294  pcqmul  12302  pcqcl  12305  pcxnn0cl  12309  pcge0  12311  pcdvdsb  12318  pceq0  12320  pcneg  12323  pcdvdstr  12325  pcgcd1  12326  pc2dvds  12328  pcz  12330  pcprmpw2  12331  pcaddlem  12337  pcadd  12338  pcmptcl  12339  pcmpt  12340  pcmptdvds  12342  fldivp1  12345  qexpz  12349  pockthlem  12353  pockthg  12354  prmunb  12359  1arith  12364  ennnfonelemom  12408  ennnfoneleminc  12411  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemdm  12420  ennnfonelemr  12423  ennnfonelemim  12424  exmidunben  12426  ctinfom  12428  inffinp1  12429  ctinf  12430  enctlem  12432  ctiunctlemu1st  12434  ctiunctlemu2nd  12435  ctiunctlemudc  12437  ctiunct  12440  ctiunctal  12441  unct  12442  ssomct  12445  nninfdclemcl  12448  nninfdclemp1  12450  nninfdc  12453  structcnvcnv  12477  setscom  12501  ressbas2d  12527  ressval3d  12530  ressabsg  12534  restid2  12696  imasaddfnlemg  12734  quslem  12744  ercpbl  12749  fnpr2ob  12758  mgmplusf  12784  grprinvlem  12803  grprinvd  12804  grpridd  12805  ismnd  12819  mhmpropd  12856  grppropd  12892  grpsubf  12948  dfgrp3mlem  12967  mulgnn0p1  12993  mulgnn0subcl  12995  mulgsubcl  12996  mulgneg  13000  mulgnn0dir  13011  mulgnn0ass  13017  issubg2m  13047  issubg4m  13051  lringuplu  13335  topontopon  13456  eltg3i  13492  epttop  13526  difopn  13544  uncld  13549  0nnei  13589  resttopon  13607  restabs  13611  restopnb  13617  lmcvg  13653  cnptopco  13658  cnss1  13662  cnss2  13663  cncnpi  13664  cncnp2m  13667  cnrest  13671  cnrest2  13672  cnrest2r  13673  cnptoprest  13675  cnptoprest2  13676  lmss  13682  lmff  13685  lmtopcnp  13686  lmcn  13687  txbasval  13703  upxp  13708  txcnmpt  13709  txdis1cn  13714  txlm  13715  lmcn2  13716  cnmpt11  13719  cnmpt11f  13720  cnmpt1t  13721  cnmpt12  13723  cnmpt21  13727  cnmpt21f  13728  cnmpt2t  13729  cnmpt22  13730  cnmpt22f  13731  cnmptcom  13734  hmeocnv  13743  hmeof1o  13745  hmeores  13751  txhmeo  13755  txswaphmeo  13757  isxmet2d  13784  blfvalps  13821  xblss2ps  13840  xblss2  13841  blfps  13845  blf  13846  unirnblps  13858  unirnbl  13859  isxms2  13888  bdxmet  13937  bdmet  13938  xmetxp  13943  xmettx  13946  blssioo  13981  tgioo  13982  mulcncflem  14026  dedekindeulemuub  14031  dedekindeulemub  14032  dedekindeulemloc  14033  dedekindeulemlu  14035  suplociccreex  14038  suplociccex  14039  dedekindicclemuub  14040  dedekindicclemub  14041  dedekindicclemloc  14042  dedekindicclemlu  14044  dedekindicc  14047  ivthinclemlopn  14050  ivthinclemuopn  14052  limcrcl  14063  limcmpted  14068  limccnp2lem  14081  limccnp2cntop  14082  limccoap  14083  dvrecap  14113  cosordlem  14206  logbgcd1irraplemexp  14322  logbgcd1irrap  14324  lgsneg1  14362  lgsdilem  14364  lgsdir2  14370  lgsdirprm  14371  lgsdir  14372  lgsne0  14375  lgsabs1  14376  lgsdirnn0  14384  lgsdinn0  14385  lgseisenlem1  14386  2sqlem5  14402  2sqlem7  14404  2sqlem8a  14405  2sqlem8  14406  2sqlem9  14407  bj-stand  14436  bj-charfundcALT  14497  bj-charfunbi  14499  bj-bdfindis  14635  bj-peano4  14643  strcollnfALT  14674  pwtrufal  14683  pwf1oexmid  14685  subctctexmid  14686  pw1nct  14688  nnsf  14690  nninfalllem1  14693  nninfall  14694  nninfsellemqall  14700  exmidsbthrlem  14706  sbthom  14710  cvgcmp2nlemabs  14716  trilpo  14727  iswomni0  14735  redcwlpo  14739  dceqnconst  14743  dcapnconst  14744  nconstwlpolem  14748  nconstwlpo  14749  neapmkvlem  14750  neapmkv  14751  ltlenmkv  14753  taupi  14756  alsi1d  14764  alsi2d  14765  alsc1d  14766  alsc2d  14767