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  7319  suplubti  7341  supelti  7343  infmoti  7369  infisoti  7373  djulclb  7396  updjud  7423  omp1eomlem  7435  0ct  7448  ctmlemr  7449  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumct  7456  nninfninc  7464  nnnninfeq2  7470  finomni  7481  fodjuomnilemdc  7485  fodjum  7487  fodjuomnilemres  7489  fodjumkvlemres  7500  omniwomnimkv  7508  nninfwlporlem  7514  nninfwlpoimlemginf  7517  nninfwlpoim  7520  nninfinfwlpo  7521  ficardon  7535  pr2cv1  7542  exmidonfinlem  7546  en2eleq  7548  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemim  7554  finacn  7561  acfun  7564  exmidaclem  7565  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  pw1if  7585  pw1on  7586  papsym  7613  papcotr  7614  dftap2  7618  2omotaplemst  7625  exmidapne  7627  ccfunen  7631  cc1  7632  cc2lem  7633  cc2  7634  cc3  7635  acnccim  7639  elni2  7682  indpi  7710  distrnqg  7755  subhalfnqq  7782  enq0sym  7800  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  nnnq0lem1  7814  distrnq0  7827  elinp  7842  elnp1st2nd  7844  prltlu  7855  prnmaxl  7856  prnminu  7857  prarloc  7871  nqprm  7910  appdivnq  7931  prmuloc  7934  mullocpr  7939  distrlem4prl  7952  distrlem4pru  7953  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemdisj  8019  cauappcvgprlem2  8028  cauappcvgprlemlim  8029  caucvgprlemnkj  8034  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemdisj  8042  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem2  8048  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemlol  8066  caucvgprprlemexbt  8074  caucvgprprlem1  8077  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  prsrlem1  8110  gt0srpr  8116  caucvgsrlemcl  8157  caucvgsrlembound  8162  caucvgsrlemgt1  8163  suplocsrlemb  8174  suplocsrlem  8176  suplocsr  8177  ltresr  8207  nnindnn  8261  axcaucvglemcl  8263  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  sup3exmid  9290  indconst0  9305  indconst1  9306  nnind  9323  nn0supp  9624  nn0ge2m1nn  9632  zleloe  9696  zapne  9724  nn0lt2  9732  suprzclex  9749  zindd  9769  uzm1  9963  uzin  9965  infregelbex  10008  elnn1uz2  10017  nn01to3  10027  divfnzn  10031  qapne  10049  irraddap  10057  xrltnsym2  10207  xaddass  10282  xleadd1a  10286  xlt2add  10293  xlesubadd  10296  iooval2  10328  icoshftf1o  10404  fztri3or  10454  fzneuz  10519  4fvwrd4  10558  elfzo0  10604  infssuzex  10677  infssuzcldc  10679  infssfzcldc  10680  infssfzledc  10681  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  exbtwnzlemex  10695  ioom  10706  fzfig  10882  uzennn  10888  uzsinds  10896  iseqovex  10910  seq3val  10912  seqvalcd  10913  seqf  10916  seqovcd  10919  monoord2  10938  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seq3f1olemqsum  10965  seq3f1o  10969  seqf1og  10973  seq3distr  10984  expp1  10998  expcl2lemap  11003  expclzap  11016  expap0i  11023  nn0ltexp2  11163  bcval5  11217  hashinfuni  11232  hashennnuni  11234  hashnncl  11250  resunimafz0  11290  hashf1lem2  11302  hashf1  11303  zfz1isolemiso  11307  zfz1isolem1  11308  zfz1iso  11309  wrdsymb0  11353  wrdlen1  11358  ccat1st1st  11425  swrdrlen  11449  pfxid  11474  pfxwrdsymbg  11478  pfxtrcfv  11481  pfxccat1  11490  pfxpfxid  11497  pfxcctswrd  11498  swrdccatin1  11513  pfxccatin12  11521  pfxccatid  11529  seq3shft  11619  cvg1nlemcau  11766  rexanuz  11770  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemsqa  11806  resqrexlemex  11807  rersqreu  11810  caubnd2  11900  maxleast  11996  fimaxre2  12010  minmax  12014  xrmaxiflemcl  12030  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxadd  12046  xrminmax  12050  xrbdtri  12061  climreu  12082  reccn2ap  12098  iserex  12124  climcvg1nlem  12134  serf0  12137  fz1f1o  12160  summodclem3  12166  zsumdc  12170  fsum3  12173  isumz  12175  isumss  12177  isumss2  12179  fsumsersdc  12181  fsum3ser  12183  fsumsplit  12193  isumclim2  12208  isumclim3  12209  fsum2dlemstep  12220  fsumcnv  12223  fisumcom2  12224  bcxmas  12275  isumle  12281  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratz  12318  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  zproddc  12365  prod1dc  12372  fprodsplitdc  12382  fprodsplit  12383  fprodunsn  12390  fprodcl2lem  12391  fprodcllemf  12399  fprod2dlemstep  12408  fprodcnv  12411  fprodcom2fi  12412  fprodle  12426  ef0lem  12446  fsumdvds  12628  mod2eq1n2dvds  12665  ndvdssub  12716  bitsfzolem  12740  bitsfzo  12741  bitsinv1  12748  gcdsupex  12753  gcdsupcl  12754  bezoutlemnewy  12792  bezoutlemmain  12794  bezoutlembi  12801  bezoutlemeu  12803  bezoutlemle  12804  uzwodc  12833  nnwofdc  12834  nnwosdc  12835  nninfctlemfo  12836  nninfct  12837  nn0seqcvgd  12838  eucalgf  12852  eucalginv  12853  lcmval  12860  prmind2  12917  dfphi2  13021  phiprmpw  13023  phimullem  13026  eulerthlem1  13028  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  eulerth  13034  phisum  13042  odzcllem  13044  odzdvds  13047  pythagtriplem19  13084  pclemub  13089  pcprecl  13091  pceu  13097  pcqmul  13105  pcqcl  13108  pcxnn0cl  13112  pcxqcl  13114  pcge0  13115  pcdvdsb  13122  pceq0  13124  pcneg  13127  pcdvdstr  13129  pcgcd1  13130  pc2dvds  13132  pcz  13134  pcprmpw2  13135  pcaddlem  13141  pcadd  13142  pcmptcl  13144  pcmpt  13145  pcmptdvds  13147  fldivp1  13150  qexpz  13154  pockthlem  13158  pockthg  13159  prmunb  13164  1arith  13169  4sqlemffi  13198  4sqlem17  13209  4sqlem18  13210  4sqlem19  13211  prmlem1a  13244  ballotfilemcdc  13275  ballotfilem2  13280  ballotfilemfp1  13283  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfmpn  13286  ballotfilemefi  13289  ballotfilemiex  13296  ballotfilemro  13318  ennnfonelemom  13351  ennnfoneleminc  13354  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemdm  13363  ennnfonelemr  13366  ennnfonelemim  13367  exmidunben  13369  ctinfom  13371  inffinp1  13372  ctinf  13373  enctlem  13375  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunct  13383  ctiunctal  13384  unct  13385  ssomct  13388  nninfdclemcl  13391  nninfdclemp1  13393  nninfdc  13396  structcnvcnv  13420  setscom  13444  relelbasov  13468  ressbas2d  13475  ressval3d  13479  ressabsg  13483  restid2  13655  imasaddfnlemg  13688  quslem  13698  ercpbl  13705  fnpr2ob  13714  mgmplusf  13739  grpinvalem  13758  grpinva  13759  grprida  13760  fngzsum  13761  gzsumvalx  13762  gzsum0  13766  gzsumval2  13767  ismnd  13785  mhmpropd  13826  grppropd  13875  grpsubf  13937  dfgrp3mlem  13956  mulgnn0p1  13989  mulgnn0subcl  13991  mulgsubcl  13992  mulgneg  13996  mulgnn0dir  14008  mulgnn0ass  14014  submmulg  14022  issubg2m  14045  issubg4m  14049  ghmmulg  14112  ghmrn  14113  gsumvalfi  14236  gzsumgsum  14239  gsumf1ofi  14244  gsummhmfi  14248  gsumressfi  14251  lringuplu  14587  rrgsupp  14658  opprdrng  14704  lmodscaf  14731  lssintclm  14805  lspun0  14846  lidlbas  14899  psrbagconcl  15148  psr1clfi  15170  topontopon  15212  eltg3i  15248  epttop  15282  difopn  15300  uncld  15305  0nnei  15345  resttopon  15363  restabs  15367  restopnb  15373  lmcvg  15409  cnptopco  15414  cnss1  15418  cnss2  15419  cncnpi  15420  cncnp2m  15423  cnrest  15427  cnrest2  15428  cnrest2r  15429  cnptoprest  15431  cnptoprest2  15432  lmss  15438  lmff  15441  lmtopcnp  15442  lmcn  15443  txbasval  15459  upxp  15464  txcnmpt  15465  txdis1cn  15470  txlm  15471  lmcn2  15472  cnmpt11  15475  cnmpt11f  15476  cnmpt1t  15477  cnmpt12  15479  cnmpt21  15483  cnmpt21f  15484  cnmpt2t  15485  cnmpt22  15486  cnmpt22f  15487  cnmptcom  15490  hmeocnv  15499  hmeof1o  15501  hmeores  15507  txhmeo  15511  txswaphmeo  15513  isxmet2d  15540  blfvalps  15577  xblss2ps  15596  xblss2  15597  blfps  15601  blf  15602  unirnblps  15614  unirnbl  15615  isxms2  15644  bdxmet  15693  bdmet  15694  xmetxp  15699  xmettx  15702  blssioo  15745  tgioo  15746  mulcncflem  15799  divcncfap  15806  dedekindeulemuub  15809  dedekindeulemub  15810  dedekindeulemloc  15811  dedekindeulemlu  15813  suplociccreex  15816  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemub  15819  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthdich  15845  limcrcl  15850  limcmpted  15855  limccnp2lem  15868  limccnp2cntop  15869  limccoap  15870  dvrecap  15905  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  plyco  15951  plycj  15953  plyrecj  15955  dvply1  15957  dvply2g  15958  cosordlem  16042  logbgcd1irraplemexp  16165  logbgcd1irrap  16167  zprmlogbaplem2  16177  zprmlogbaplem3  16178  birthdaylem2  16187  birthdaylem3  16188  chtqge0  16208  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  chtqwordi  16224  ppiqltx  16242  bposlem2  16273  lgsneg1  16310  lgsdilem  16312  lgsdir2  16318  lgsdirprm  16319  lgsdir  16320  lgsne0  16323  lgsabs1  16324  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1f1o  16345  gausslemma2dlem4  16349  lgseisenlem1  16355  lgsquadlem3  16364  2lgslem1a  16373  2sqlem5  16404  2sqlem7  16406  2sqlem8a  16407  2sqlem8  16408  2sqlem9  16409  gropeld  16456  grstructeld2dom  16457  uhgrm  16485  upgrm  16507  upgr1een  16531  uhgredgm  16543  edgupgren  16548  edgumgren  16549  edgusgren  16570  ausgrusgrben  16575  umgr2edg1  16616  usgredg2vlem1  16629  uhgr0enedgfi  16643  subupgr  16680  vtxedgfi  16696  vtxlpfi  16697  vtxdumgrfival  16705  vtxd0nedgbfi  16706  1hevtxdg0fi  16714  p1evtxdeqfilem  16718  wlkvtxm  16747  g0wlk0  16777  wlkres  16786  trlreslem  16796  clwwlkccatlem  16807  clwwlknnn  16819  trlsegvdeglem6  16872  eupth2lem3lem3fi  16877  eupth2lem3lem7fi  16881  eulerpathum  16888  dichmul0or  16926  bj-stand  16942  bj-charfundcALT  17001  bj-charfunbi  17003  bj-bdfindis  17139  bj-peano4  17147  strcollnfALT  17178  pw1map  17191  pwtrufal  17193  pwf1oexmid  17195  subctctexmid  17196  pw1nct  17199  stnot  17205  wexmiddc  17208  nnsf  17214  nninfalllem1  17217  nninfall  17218  nninfsellemqall  17224  nnnninfen  17230  exmidsbthrlem  17233  sbthom  17237  repiecef  17243  cvgcmp2nlemabs  17247  trilpo  17259  iswomni0  17268  redcwlpo  17272  dceqnconst  17277  dcapnconst  17278  nconstwlpolem  17282  nconstwlpo  17283  neapmkvlem  17284  neapmkv  17285  ltlenmkv  17287  taupi  17290  als1d  17300  als2d  17301  rals1d  17302  rals2d  17303  alseu1d  17336  alseu2d  17337  ralseu1d  17338  ralseu2d  17339  dfalseu2  17344