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  9287  indconst0  9302  indconst1  9303  nnind  9320  nn0supp  9619  nn0ge2m1nn  9627  zleloe  9691  zapne  9719  nn0lt2  9727  suprzclex  9744  zindd  9764  uzm1  9953  uzin  9955  infregelbex  9998  elnn1uz2  10007  nn01to3  10017  divfnzn  10021  qapne  10039  xrltnsym2  10196  xaddass  10271  xleadd1a  10275  xlt2add  10282  xlesubadd  10285  iooval2  10317  icoshftf1o  10393  fztri3or  10443  fzneuz  10508  4fvwrd4  10547  elfzo0  10593  infssuzex  10666  infssuzcldc  10668  infssfzcldc  10669  infssfzledc  10670  suprzubdc  10671  nninfdcex  10672  zsupssdc  10673  exbtwnzlemex  10684  ioom  10695  fzfig  10867  uzennn  10873  uzsinds  10881  iseqovex  10895  seq3val  10897  seqvalcd  10898  seqf  10901  seqovcd  10904  monoord2  10923  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seq3f1olemqsum  10950  seq3f1o  10954  seqf1og  10958  seq3distr  10969  expp1  10983  expcl2lemap  10988  expclzap  11001  expap0i  11008  nn0ltexp2  11147  bcval5  11201  hashinfuni  11216  hashennnuni  11218  hashnncl  11234  resunimafz0  11274  hashf1lem2  11286  hashf1  11287  zfz1isolemiso  11291  zfz1isolem1  11292  zfz1iso  11293  wrdsymb0  11337  wrdlen1  11342  ccat1st1st  11409  swrdrlen  11433  pfxid  11458  pfxwrdsymbg  11462  pfxtrcfv  11465  pfxccat1  11474  pfxpfxid  11481  pfxcctswrd  11482  swrdccatin1  11497  pfxccatin12  11505  pfxccatid  11513  seq3shft  11603  cvg1nlemcau  11750  rexanuz  11754  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  rersqreu  11794  caubnd2  11883  maxleast  11979  fimaxre2  11993  minmax  11996  xrmaxiflemcl  12011  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxadd  12027  xrminmax  12031  xrbdtri  12042  climreu  12063  reccn2ap  12079  iserex  12105  climcvg1nlem  12115  serf0  12118  fz1f1o  12141  summodclem3  12147  zsumdc  12151  fsum3  12154  isumz  12156  isumss  12158  isumss2  12160  fsumsersdc  12162  fsum3ser  12164  fsumsplit  12174  isumclim2  12189  isumclim3  12190  fsum2dlemstep  12201  fsumcnv  12204  fisumcom2  12205  bcxmas  12256  isumle  12262  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratz  12299  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  zproddc  12346  prod1dc  12353  fprodsplitdc  12363  fprodsplit  12364  fprodunsn  12371  fprodcl2lem  12372  fprodcllemf  12380  fprod2dlemstep  12389  fprodcnv  12392  fprodcom2fi  12393  fprodle  12407  ef0lem  12427  fsumdvds  12609  mod2eq1n2dvds  12646  ndvdssub  12697  bitsfzolem  12721  bitsfzo  12722  bitsinv1  12729  gcdsupex  12734  gcdsupcl  12735  bezoutlemnewy  12773  bezoutlemmain  12775  bezoutlembi  12782  bezoutlemeu  12784  bezoutlemle  12785  uzwodc  12814  nnwofdc  12815  nnwosdc  12816  nninfctlemfo  12817  nninfct  12818  nn0seqcvgd  12819  eucalgf  12833  eucalginv  12834  lcmval  12841  prmind2  12898  dfphi2  12998  phiprmpw  13000  phimullem  13003  eulerthlem1  13005  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  eulerth  13011  phisum  13019  odzcllem  13021  odzdvds  13024  pythagtriplem19  13061  pclemub  13066  pcprecl  13068  pceu  13074  pcqmul  13082  pcqcl  13085  pcxnn0cl  13089  pcxqcl  13091  pcge0  13092  pcdvdsb  13099  pceq0  13101  pcneg  13104  pcdvdstr  13106  pcgcd1  13107  pc2dvds  13109  pcz  13111  pcprmpw2  13112  pcaddlem  13118  pcadd  13119  pcmptcl  13121  pcmpt  13122  pcmptdvds  13124  fldivp1  13127  qexpz  13131  pockthlem  13135  pockthg  13136  prmunb  13141  1arith  13146  4sqlemffi  13175  4sqlem17  13186  4sqlem18  13187  4sqlem19  13188  ballotfilemcdc  13223  ballotfilem2  13228  ballotfilemfp1  13231  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfmpn  13234  ballotfilemefi  13237  ballotfilemiex  13244  ballotfilemro  13266  ennnfonelemom  13299  ennnfoneleminc  13302  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemdm  13311  ennnfonelemr  13314  ennnfonelemim  13315  exmidunben  13317  ctinfom  13319  inffinp1  13320  ctinf  13321  enctlem  13323  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  ctiunctlemudc  13328  ctiunct  13331  ctiunctal  13332  unct  13333  ssomct  13336  nninfdclemcl  13339  nninfdclemp1  13341  nninfdc  13344  structcnvcnv  13368  setscom  13392  relelbasov  13416  ressbas2d  13422  ressval3d  13426  ressabsg  13430  restid2  13602  imasaddfnlemg  13635  quslem  13645  ercpbl  13652  fnpr2ob  13661  mgmplusf  13686  grpinvalem  13705  grpinva  13706  grprida  13707  fngzsum  13708  gzsumvalx  13709  gzsum0  13713  gzsumval2  13714  ismnd  13732  mhmpropd  13773  grppropd  13822  grpsubf  13884  dfgrp3mlem  13903  mulgnn0p1  13936  mulgnn0subcl  13938  mulgsubcl  13939  mulgneg  13943  mulgnn0dir  13955  mulgnn0ass  13961  submmulg  13969  issubg2m  13992  issubg4m  13996  ghmmulg  14059  ghmrn  14060  gsumvalfi  14152  gzsumgsum  14155  gsumf1ofi  14160  gsummhmfi  14164  gsumressfi  14167  lringuplu  14503  rrgsupp  14574  opprdrng  14620  lmodscaf  14647  lssintclm  14721  lspun0  14762  lidlbas  14815  psrbagconcl  15063  psr1clfi  15079  topontopon  15121  eltg3i  15157  epttop  15191  difopn  15209  uncld  15214  0nnei  15254  resttopon  15272  restabs  15276  restopnb  15282  lmcvg  15318  cnptopco  15323  cnss1  15327  cnss2  15328  cncnpi  15329  cncnp2m  15332  cnrest  15336  cnrest2  15337  cnrest2r  15338  cnptoprest  15340  cnptoprest2  15341  lmss  15347  lmff  15350  lmtopcnp  15351  lmcn  15352  txbasval  15368  upxp  15373  txcnmpt  15374  txdis1cn  15379  txlm  15380  lmcn2  15381  cnmpt11  15384  cnmpt11f  15385  cnmpt1t  15386  cnmpt12  15388  cnmpt21  15392  cnmpt21f  15393  cnmpt2t  15394  cnmpt22  15395  cnmpt22f  15396  cnmptcom  15399  hmeocnv  15408  hmeof1o  15410  hmeores  15416  txhmeo  15420  txswaphmeo  15422  isxmet2d  15449  blfvalps  15486  xblss2ps  15505  xblss2  15506  blfps  15510  blf  15511  unirnblps  15523  unirnbl  15524  isxms2  15553  bdxmet  15602  bdmet  15603  xmetxp  15608  xmettx  15611  blssioo  15654  tgioo  15655  mulcncflem  15708  divcncfap  15715  dedekindeulemuub  15718  dedekindeulemub  15719  dedekindeulemloc  15720  dedekindeulemlu  15722  suplociccreex  15725  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemub  15728  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthdich  15754  limcrcl  15759  limcmpted  15764  limccnp2lem  15777  limccnp2cntop  15778  limccoap  15779  dvrecap  15814  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  plyco  15860  plycj  15862  plyrecj  15864  dvply1  15866  dvply2g  15867  cosordlem  15950  logbgcd1irraplemexp  16070  logbgcd1irrap  16072  birthdaylem2  16088  birthdaylem3  16089  lgsneg1  16144  lgsdilem  16146  lgsdir2  16152  lgsdirprm  16153  lgsdir  16154  lgsne0  16157  lgsabs1  16158  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1f1o  16179  gausslemma2dlem4  16183  lgseisenlem1  16189  lgsquadlem3  16198  2lgslem1a  16207  2sqlem5  16238  2sqlem7  16240  2sqlem8a  16241  2sqlem8  16242  2sqlem9  16243  gropeld  16290  grstructeld2dom  16291  uhgrm  16319  upgrm  16341  upgr1een  16365  uhgredgm  16377  edgupgren  16382  edgumgren  16383  edgusgren  16404  ausgrusgrben  16409  umgr2edg1  16450  usgredg2vlem1  16463  uhgr0enedgfi  16477  subupgr  16514  vtxedgfi  16530  vtxlpfi  16531  vtxdumgrfival  16539  vtxd0nedgbfi  16540  1hevtxdg0fi  16548  p1evtxdeqfilem  16552  wlkvtxm  16581  g0wlk0  16611  wlkres  16620  trlreslem  16630  clwwlkccatlem  16641  clwwlknnn  16653  trlsegvdeglem6  16706  eupth2lem3lem3fi  16711  eupth2lem3lem7fi  16715  eulerpathum  16722  dichmul0or  16760  bj-stand  16776  bj-charfundcALT  16835  bj-charfunbi  16837  bj-bdfindis  16973  bj-peano4  16981  strcollnfALT  17012  pw1map  17025  pwtrufal  17027  pwf1oexmid  17029  subctctexmid  17030  pw1nct  17033  stnot  17039  wexmiddc  17042  nnsf  17048  nninfalllem1  17051  nninfall  17052  nninfsellemqall  17058  nnnninfen  17064  exmidsbthrlem  17067  sbthom  17071  repiecef  17077  cvgcmp2nlemabs  17081  trilpo  17092  iswomni0  17101  redcwlpo  17105  dceqnconst  17110  dcapnconst  17111  nconstwlpolem  17115  nconstwlpo  17116  neapmkvlem  17117  neapmkv  17118  ltlenmkv  17120  taupi  17123  als1d  17133  als2d  17134  rals1d  17135  rals2d  17136  alseu1d  17169  alseu2d  17170  ralseu1d  17171  ralseu2d  17172  dfalseu2  17177