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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb1  137  bicomd  141  pm5.74d  182  bitri  184  3imtr3i  200  ancomd  267  pm4.71d  397  pm4.71rd  398  imdistand  451  orcomd  741  3mix3  1199  mpjao3dan  1348  ecase23d  1391  exlimdh  1649  nexd  1666  alexnim  1701  excomim  1715  19.41  1738  equcomd  1759  nfexd  1814  sbh  1829  sbcof2  1863  sbidm  1904  sb6rf  1906  nfsbt  2036  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eu2  2131  2euex  2174  eqcomd  2244  3eltr3g  2323  abbid  2355  neneqd  2441  eqnetrrid  2451  3netr3g  2454  necomd  2506  r19.21bi  2638  nrexdv  2643  rexlimd  2665  rabbidva  2809  elisset  2836  euind  3013  rmoan  3026  reuind  3031  2rmorex  3032  spsbc  3063  spesbc  3138  eldifad  3231  eldifbd  3232  3sstr3g  3290  sseqtrdi  3296  difindiss  3485  un00  3567  vvin  3569  undifss  3608  ifcldcd  3678  disjpr2  3773  difprsn1  3854  diftpsn3  3856  difsnss  3861  sneqr  3885  preqr1  3893  preq12b  3895  oprcl  3928  intab  3999  riinm  4085  rintm  4105  disjiun  4125  sndisj  4126  3brtr3g  4163  trint  4244  iinexgm  4290  exmidexmid  4333  exmid01  4335  pwntru  4336  exmid1stab  4345  pwel  4358  exss  4367  0nelop  4388  euotd  4395  opelopabsb  4402  pwunim  4431  issod  4464  frind  4497  suctr  4566  orduniss  4570  onelini  4575  oneluni  4576  eusv2i  4601  rexxfrd  4609  rabxfrd  4615  reuhypd  4617  iunpw  4626  sucexg  4645  ordsucim  4647  ordtriexmidlem  4666  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsucunielexmid  4678  orddif  4694  suc11g  4704  onintexmid  4720  reg3exmidlemwe  4726  tfisi  4734  peano1  4741  peano2  4742  finds2  4748  omsinds  4769  brrelex12  4813  brel  4827  ssrel  4863  ssrel2  4865  ssrelrel  4875  elrel  4877  xpsspw  4887  relop  4930  dmxpm  5002  opelresi  5074  mptimass  5139  ndmima  5164  poirr2  5180  xpmlem  5208  xpimasn  5236  iotass  5355  iotacl  5362  dffun5r  5389  funeu  5402  funeu2  5403  funfnd  5408  funopg  5411  funun  5422  fununfun  5424  funinsn  5430  funtp  5434  funcnvuni  5450  funcnvres2  5456  imadiflem  5460  imadif  5461  funimaexglem  5464  fneu2  5488  fnimaeq0  5505  fnmpt  5510  ffrn  5545  fun2  5562  f00  5584  f0bi  5585  fimadmfo  5624  foimacnv  5657  resdif  5661  f1ococnv1  5668  fv3  5718  relelfvdm  5727  elfvm  5729  nfvres  5732  dffn5im  5748  mptfvex  5791  fvmptdf  5793  fvmptdv2  5795  fndmdif  5814  dff4im  5854  fmpt  5858  fmptd  5862  fmptdf  5865  f1oresrab  5873  fcoconst  5879  fsn  5880  funopsn  5891  ftpg  5899  fsnunf  5915  resfunexg  5936  mptmex  5945  isores1  6020  riota2df  6060  acexmidlemcase  6080  brabvv  6134  funoprabg  6187  fnovim  6197  ovmpodf  6220  ovi3  6226  elmpocl  6284  uchoice  6371  1stcof  6397  2ndcof  6398  opabn1stprc  6429  fnmpo  6438  fmpoco  6452  fo2ndf  6463  f1o2ndf1  6464  disjxp1  6472  fvdifsuppst  6484  fsuppeq  6487  fsuppeqg  6488  suppssrst  6501  suppssrgst  6502  brtpos2  6522  reldmtpos  6524  dftpos3  6533  dftpos4  6534  tpostpos2  6536  tposf2  6539  tposf12  6540  tposfo  6542  tposf  6543  smores2  6565  tfrlem1  6579  tfrlem3-2d  6583  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcldm  6634  rdgivallem  6652  rdgisucinc  6656  frecabex  6669  frecfnom  6672  frecfcllem  6675  frecsuclem  6677  omsuc  6745  nntri2  6767  nnsucuniel  6768  nnsseleq  6774  nnm00  6803  ecexr  6812  swoer  6835  elqsn0m  6877  iinerm  6881  erinxp  6883  ecinxp  6884  eroveu  6900  eroprf  6902  mapprc  6926  mapsn  6972  ixpprc  7001  ixp0  7013  resixp  7015  elixpsn  7017  dom2lem  7058  fundmen  7094  1dom1el  7107  dom0  7138  xpf1o  7144  mapxpen  7148  xpmapenlem  7149  ssenen  7152  nneneq  7158  ssfilem  7177  ssfilemd  7179  dif1en  7183  dif1enen  7184  fin0  7189  fin0or  7190  diffitest  7191  diffisn  7197  ac6sfi  7202  fimax2gtrilemstep  7205  fimax2gtri  7206  finexdc  7207  eqsndc  7210  exmidpweq  7216  pw1fin  7217  onunsnss  7224  unsnfidcel  7228  undifdcss  7230  undifdc  7231  tpfidceq  7237  fiintim  7238  fisseneq  7242  fidcenumlemr  7272  sbthlemi4  7277  sbthlemi5  7278  sbthlemi9  7282  fifo  7314  2omap  7318  suplubti  7340  supelti  7342  infmoti  7368  infisoti  7372  djulclb  7395  updjud  7422  omp1eomlem  7434  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumct  7455  nninfninc  7463  nnnninfeq2  7469  finomni  7480  fodjuomnilemdc  7484  fodjum  7486  fodjuomnilemres  7488  fodjumkvlemres  7499  omniwomnimkv  7507  nninfwlporlem  7513  nninfwlpoimlemginf  7516  nninfwlpoim  7519  nninfinfwlpo  7520  ficardon  7534  pr2cv1  7541  exmidonfinlem  7545  en2eleq  7547  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemim  7553  finacn  7560  acfun  7563  exmidaclem  7564  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  pw1if  7584  pw1on  7585  papsym  7612  papcotr  7613  dftap2  7617  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  cc1  7631  cc2lem  7632  cc2  7633  cc3  7634  acnccim  7638  elni2  7681  indpi  7709  distrnqg  7754  subhalfnqq  7781  enq0sym  7799  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nnnq0lem1  7813  distrnq0  7826  elinp  7841  elnp1st2nd  7843  prltlu  7854  prnmaxl  7855  prnminu  7856  prarloc  7870  nqprm  7909  appdivnq  7930  prmuloc  7933  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemlol  8065  caucvgprprlemexbt  8073  caucvgprprlem1  8076  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  prsrlem1  8109  gt0srpr  8115  caucvgsrlemcl  8156  caucvgsrlembound  8161  caucvgsrlemgt1  8162  suplocsrlemb  8173  suplocsrlem  8175  suplocsr  8176  ltresr  8206  nnindnn  8260  axcaucvglemcl  8262  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  sup3exmid  9289  indconst0  9304  indconst1  9305  nnind  9322  nn0supp  9623  nn0ge2m1nn  9631  zleloe  9695  zapne  9723  nn0lt2  9731  suprzclex  9748  zindd  9768  uzm1  9962  uzin  9964  infregelbex  10007  elnn1uz2  10016  nn01to3  10026  divfnzn  10030  qapne  10048  irraddap  10056  xrltnsym2  10206  xaddass  10281  xleadd1a  10285  xlt2add  10292  xlesubadd  10295  iooval2  10327  icoshftf1o  10403  fztri3or  10453  fzneuz  10518  4fvwrd4  10557  elfzo0  10603  infssuzex  10676  infssuzcldc  10678  infssfzcldc  10679  infssfzledc  10680  suprzubdc  10681  nninfdcex  10682  zsupssdc  10683  exbtwnzlemex  10694  ioom  10705  fzfig  10880  uzennn  10886  uzsinds  10894  iseqovex  10908  seq3val  10910  seqvalcd  10911  seqf  10914  seqovcd  10917  monoord2  10936  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seq3f1olemqsum  10963  seq3f1o  10967  seqf1og  10971  seq3distr  10982  expp1  10996  expcl2lemap  11001  expclzap  11014  expap0i  11021  nn0ltexp2  11161  bcval5  11215  hashinfuni  11230  hashennnuni  11232  hashnncl  11248  resunimafz0  11288  hashf1lem2  11300  hashf1  11301  zfz1isolemiso  11305  zfz1isolem1  11306  zfz1iso  11307  wrdsymb0  11351  wrdlen1  11356  ccat1st1st  11423  swrdrlen  11447  pfxid  11472  pfxwrdsymbg  11476  pfxtrcfv  11479  pfxccat1  11488  pfxpfxid  11495  pfxcctswrd  11496  swrdccatin1  11511  pfxccatin12  11519  pfxccatid  11527  seq3shft  11617  cvg1nlemcau  11764  rexanuz  11768  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemsqa  11804  resqrexlemex  11805  rersqreu  11808  caubnd2  11898  maxleast  11994  fimaxre2  12008  minmax  12011  xrmaxiflemcl  12027  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxadd  12043  xrminmax  12047  xrbdtri  12058  climreu  12079  reccn2ap  12095  iserex  12121  climcvg1nlem  12131  serf0  12134  fz1f1o  12157  summodclem3  12163  zsumdc  12167  fsum3  12170  isumz  12172  isumss  12174  isumss2  12176  fsumsersdc  12178  fsum3ser  12180  fsumsplit  12190  isumclim2  12205  isumclim3  12206  fsum2dlemstep  12217  fsumcnv  12220  fisumcom2  12221  bcxmas  12272  isumle  12278  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratz  12315  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  zproddc  12362  prod1dc  12369  fprodsplitdc  12379  fprodsplit  12380  fprodunsn  12387  fprodcl2lem  12388  fprodcllemf  12396  fprod2dlemstep  12405  fprodcnv  12408  fprodcom2fi  12409  fprodle  12423  ef0lem  12443  fsumdvds  12625  mod2eq1n2dvds  12662  ndvdssub  12713  bitsfzolem  12737  bitsfzo  12738  bitsinv1  12745  gcdsupex  12750  gcdsupcl  12751  bezoutlemnewy  12789  bezoutlemmain  12791  bezoutlembi  12798  bezoutlemeu  12800  bezoutlemle  12801  uzwodc  12830  nnwofdc  12831  nnwosdc  12832  nninfctlemfo  12833  nninfct  12834  nn0seqcvgd  12835  eucalgf  12849  eucalginv  12850  lcmval  12857  prmind2  12914  dfphi2  13018  phiprmpw  13020  phimullem  13023  eulerthlem1  13025  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  eulerth  13031  phisum  13039  odzcllem  13041  odzdvds  13044  pythagtriplem19  13081  pclemub  13086  pcprecl  13088  pceu  13094  pcqmul  13102  pcqcl  13105  pcxnn0cl  13109  pcxqcl  13111  pcge0  13112  pcdvdsb  13119  pceq0  13121  pcneg  13124  pcdvdstr  13126  pcgcd1  13127  pc2dvds  13129  pcz  13131  pcprmpw2  13132  pcaddlem  13138  pcadd  13139  pcmptcl  13141  pcmpt  13142  pcmptdvds  13144  fldivp1  13147  qexpz  13151  pockthlem  13155  pockthg  13156  prmunb  13161  1arith  13166  4sqlemffi  13195  4sqlem17  13206  4sqlem18  13207  4sqlem19  13208  prmlem1a  13241  ballotfilemcdc  13272  ballotfilem2  13277  ballotfilemfp1  13280  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfmpn  13283  ballotfilemefi  13286  ballotfilemiex  13293  ballotfilemro  13315  ennnfonelemom  13348  ennnfoneleminc  13351  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemdm  13360  ennnfonelemr  13363  ennnfonelemim  13364  exmidunben  13366  ctinfom  13368  inffinp1  13369  ctinf  13370  enctlem  13372  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunct  13380  ctiunctal  13381  unct  13382  ssomct  13385  nninfdclemcl  13388  nninfdclemp1  13390  nninfdc  13393  structcnvcnv  13417  setscom  13441  relelbasov  13465  ressbas2d  13471  ressval3d  13475  ressabsg  13479  restid2  13651  imasaddfnlemg  13684  quslem  13694  ercpbl  13701  fnpr2ob  13710  mgmplusf  13735  grpinvalem  13754  grpinva  13755  grprida  13756  fngzsum  13757  gzsumvalx  13758  gzsum0  13762  gzsumval2  13763  ismnd  13781  mhmpropd  13822  grppropd  13871  grpsubf  13933  dfgrp3mlem  13952  mulgnn0p1  13985  mulgnn0subcl  13987  mulgsubcl  13988  mulgneg  13992  mulgnn0dir  14004  mulgnn0ass  14010  submmulg  14018  issubg2m  14041  issubg4m  14045  ghmmulg  14108  ghmrn  14109  gsumvalfi  14201  gzsumgsum  14204  gsumf1ofi  14209  gsummhmfi  14213  gsumressfi  14216  lringuplu  14552  rrgsupp  14623  opprdrng  14669  lmodscaf  14696  lssintclm  14770  lspun0  14811  lidlbas  14864  psrbagconcl  15112  psr1clfi  15128  topontopon  15170  eltg3i  15206  epttop  15240  difopn  15258  uncld  15263  0nnei  15303  resttopon  15321  restabs  15325  restopnb  15331  lmcvg  15367  cnptopco  15372  cnss1  15376  cnss2  15377  cncnpi  15378  cncnp2m  15381  cnrest  15385  cnrest2  15386  cnrest2r  15387  cnptoprest  15389  cnptoprest2  15390  lmss  15396  lmff  15399  lmtopcnp  15400  lmcn  15401  txbasval  15417  upxp  15422  txcnmpt  15423  txdis1cn  15428  txlm  15429  lmcn2  15430  cnmpt11  15433  cnmpt11f  15434  cnmpt1t  15435  cnmpt12  15437  cnmpt21  15441  cnmpt21f  15442  cnmpt2t  15443  cnmpt22  15444  cnmpt22f  15445  cnmptcom  15448  hmeocnv  15457  hmeof1o  15459  hmeores  15465  txhmeo  15469  txswaphmeo  15471  isxmet2d  15498  blfvalps  15535  xblss2ps  15554  xblss2  15555  blfps  15559  blf  15560  unirnblps  15572  unirnbl  15573  isxms2  15602  bdxmet  15651  bdmet  15652  xmetxp  15657  xmettx  15660  blssioo  15703  tgioo  15704  mulcncflem  15757  divcncfap  15764  dedekindeulemuub  15767  dedekindeulemub  15768  dedekindeulemloc  15769  dedekindeulemlu  15771  suplociccreex  15774  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemub  15777  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthdich  15803  limcrcl  15808  limcmpted  15813  limccnp2lem  15826  limccnp2cntop  15827  limccoap  15828  dvrecap  15863  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  plyco  15909  plycj  15911  plyrecj  15913  dvply1  15915  dvply2g  15916  cosordlem  16000  logbgcd1irraplemexp  16123  logbgcd1irrap  16125  zprmlogbaplem2  16135  zprmlogbaplem3  16136  birthdaylem2  16145  birthdaylem3  16146  ppiprm  16170  ppinprm  16171  ppiqltx  16183  bposlem2  16210  lgsneg1  16242  lgsdilem  16244  lgsdir2  16250  lgsdirprm  16251  lgsdir  16252  lgsne0  16255  lgsabs1  16256  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1f1o  16277  gausslemma2dlem4  16281  lgseisenlem1  16287  lgsquadlem3  16296  2lgslem1a  16305  2sqlem5  16336  2sqlem7  16338  2sqlem8a  16339  2sqlem8  16340  2sqlem9  16341  gropeld  16388  grstructeld2dom  16389  uhgrm  16417  upgrm  16439  upgr1een  16463  uhgredgm  16475  edgupgren  16480  edgumgren  16481  edgusgren  16502  ausgrusgrben  16507  umgr2edg1  16548  usgredg2vlem1  16561  uhgr0enedgfi  16575  subupgr  16612  vtxedgfi  16628  vtxlpfi  16629  vtxdumgrfival  16637  vtxd0nedgbfi  16638  1hevtxdg0fi  16646  p1evtxdeqfilem  16650  wlkvtxm  16679  g0wlk0  16709  wlkres  16718  trlreslem  16728  clwwlkccatlem  16739  clwwlknnn  16751  trlsegvdeglem6  16804  eupth2lem3lem3fi  16809  eupth2lem3lem7fi  16813  eulerpathum  16820  dichmul0or  16858  bj-stand  16874  bj-charfundcALT  16933  bj-charfunbi  16935  bj-bdfindis  17071  bj-peano4  17079  strcollnfALT  17110  pw1map  17123  pwtrufal  17125  pwf1oexmid  17127  subctctexmid  17128  pw1nct  17131  stnot  17137  wexmiddc  17140  nnsf  17146  nninfalllem1  17149  nninfall  17150  nninfsellemqall  17156  nnnninfen  17162  exmidsbthrlem  17165  sbthom  17169  repiecef  17175  cvgcmp2nlemabs  17179  trilpo  17190  iswomni0  17199  redcwlpo  17203  dceqnconst  17208  dcapnconst  17209  nconstwlpolem  17213  nconstwlpo  17214  neapmkvlem  17215  neapmkv  17216  ltlenmkv  17218  taupi  17221  als1d  17231  als2d  17232  rals1d  17233  rals2d  17234  alseu1d  17267  alseu2d  17268  ralseu1d  17269  ralseu2d  17270  dfalseu2  17275