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  1810  sbh  1825  sbcof2  1859  sbidm  1900  sb6rf  1902  nfsbt  2030  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  eu2  2125  2euex  2168  eqcomd  2238  3eltr3g  2317  abbid  2349  neneqd  2433  eqnetrrid  2443  3netr3g  2446  necomd  2498  r19.21bi  2630  nrexdv  2635  rexlimd  2657  rabbidva  2801  elisset  2828  euind  3004  rmoan  3017  reuind  3022  2rmorex  3023  spsbc  3054  spesbc  3129  eldifad  3222  eldifbd  3223  3sstr3g  3280  sseqtrdi  3286  difindiss  3475  un00  3555  undifss  3590  ifcldcd  3660  disjpr2  3753  difprsn1  3833  diftpsn3  3835  difsnss  3840  sneqr  3864  preqr1  3872  preq12b  3874  oprcl  3907  intab  3978  riinm  4064  rintm  4084  disjiun  4104  sndisj  4105  3brtr3g  4142  trint  4223  iinexgm  4266  exmidexmid  4309  exmid01  4311  pwntru  4312  exmid1stab  4321  pwel  4334  exss  4343  0nelop  4364  euotd  4371  opelopabsb  4378  pwunim  4407  issod  4440  frind  4473  suctr  4542  orduniss  4546  onelini  4551  oneluni  4552  eusv2i  4576  rexxfrd  4584  rabxfrd  4590  reuhypd  4592  iunpw  4601  sucexg  4620  ordsucim  4622  ordtriexmidlem  4641  ontriexmidim  4644  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  ordsucunielexmid  4653  orddif  4669  suc11g  4679  onintexmid  4695  reg3exmidlemwe  4701  tfisi  4709  peano1  4716  peano2  4717  finds2  4723  omsinds  4744  brrelex12  4788  brel  4802  ssrel  4838  ssrel2  4840  ssrelrel  4850  elrel  4852  xpsspw  4862  relop  4905  dmxpm  4977  opelresi  5049  mptimass  5114  ndmima  5139  poirr2  5155  xpmlem  5183  xpimasn  5211  iotass  5330  iotacl  5337  dffun5r  5364  funeu  5377  funeu2  5378  funfnd  5383  funopg  5386  funun  5397  fununfun  5399  funinsn  5405  funtp  5409  funcnvuni  5425  funcnvres2  5431  imadiflem  5435  imadif  5436  funimaexglem  5439  fneu2  5463  fnimaeq0  5480  fnmpt  5485  ffrn  5520  fun2  5537  f00  5559  f0bi  5560  fimadmfo  5599  foimacnv  5632  resdif  5636  f1ococnv1  5643  fv3  5693  relelfvdm  5702  elfvm  5703  nfvres  5706  dffn5im  5722  mptfvex  5763  fvmptdf  5765  fvmptdv2  5767  fndmdif  5783  dff4im  5823  fmpt  5827  fmptd  5831  fmptdf  5834  f1oresrab  5842  fcoconst  5848  fsn  5849  funopsn  5860  ftpg  5868  fsnunf  5884  resfunexg  5905  isores1  5987  riota2df  6025  acexmidlemcase  6045  brabvv  6099  funoprabg  6152  fnovim  6162  ovmpodf  6185  ovi3  6191  elmpocl  6249  uchoice  6331  1stcof  6357  2ndcof  6358  opabn1stprc  6389  fnmpo  6398  fmpoco  6412  fo2ndf  6423  f1o2ndf1  6424  disjxp1  6432  fvdifsuppst  6444  fsuppeq  6447  fsuppeqg  6448  suppssrst  6461  suppssrgst  6462  brtpos2  6482  reldmtpos  6484  dftpos3  6493  dftpos4  6494  tpostpos2  6496  tposf2  6499  tposf12  6500  tposfo  6502  tposf  6503  smores2  6525  tfrlem1  6539  tfrlem3-2d  6543  tfrlemisucaccv  6556  tfrlemibxssdm  6558  tfrlemibfn  6559  tfrlemi1  6563  tfrexlem  6565  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemaccex  6592  tfrcldm  6594  rdgivallem  6612  rdgisucinc  6616  frecabex  6629  frecfnom  6632  frecfcllem  6635  frecsuclem  6637  omsuc  6705  nntri2  6727  nnsucuniel  6728  nnsseleq  6734  nnm00  6763  ecexr  6772  swoer  6795  elqsn0m  6837  iinerm  6841  erinxp  6843  ecinxp  6844  eroveu  6860  eroprf  6862  mapprc  6886  mapsn  6925  ixpprc  6954  ixp0  6966  resixp  6968  elixpsn  6970  dom2lem  7011  fundmen  7047  1dom1el  7060  dom0  7091  xpf1o  7097  mapxpen  7101  xpmapenlem  7102  ssenen  7105  nneneq  7111  ssfilem  7130  ssfilemd  7132  dif1en  7136  dif1enen  7137  fin0  7142  fin0or  7143  diffitest  7144  diffisn  7150  ac6sfi  7155  fimax2gtrilemstep  7158  fimax2gtri  7159  finexdc  7160  eqsndc  7163  exmidpweq  7169  pw1fin  7170  onunsnss  7177  unsnfidcel  7181  undifdcss  7183  undifdc  7184  tpfidceq  7190  fiintim  7191  fisseneq  7195  fidcenumlemr  7225  sbthlemi4  7230  sbthlemi5  7231  sbthlemi9  7235  fifo  7267  2omap  7269  suplubti  7291  supelti  7293  infmoti  7319  infisoti  7323  djulclb  7346  updjud  7373  omp1eomlem  7385  0ct  7398  ctmlemr  7399  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumct  7406  nninfninc  7414  nnnninfeq2  7420  finomni  7431  fodjuomnilemdc  7435  fodjum  7437  fodjuomnilemres  7439  fodjumkvlemres  7450  omniwomnimkv  7458  nninfwlporlem  7464  nninfwlpoimlemginf  7467  nninfwlpoim  7470  nninfinfwlpo  7471  ficardon  7485  pr2cv1  7492  exmidonfinlem  7496  en2eleq  7498  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  exmidfodomrlemim  7504  finacn  7511  acfun  7514  exmidaclem  7515  exmidontriimlem3  7530  exmidontriimlem4  7531  exmidontriim  7532  pw1if  7535  pw1on  7536  papsym  7561  papcotr  7562  dftap2  7565  2omotaplemst  7572  exmidapne  7574  ccfunen  7578  cc1  7579  cc2lem  7580  cc2  7581  cc3  7582  acnccim  7586  elni2  7629  indpi  7657  distrnqg  7702  subhalfnqq  7729  enq0sym  7747  enq0ref  7748  enq0tr  7749  nqnq0pi  7753  nnnq0lem1  7761  distrnq0  7774  elinp  7789  elnp1st2nd  7791  prltlu  7802  prnmaxl  7803  prnminu  7804  prarloc  7818  nqprm  7857  appdivnq  7878  prmuloc  7881  mullocpr  7886  distrlem4prl  7899  distrlem4pru  7900  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  cauappcvgprlemopl  7961  cauappcvgprlemopu  7963  cauappcvgprlemdisj  7966  cauappcvgprlem2  7975  cauappcvgprlemlim  7976  caucvgprlemnkj  7981  caucvgprlemopl  7984  caucvgprlemopu  7986  caucvgprlemdisj  7989  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem2  7995  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemlol  8013  caucvgprprlemexbt  8021  caucvgprprlem1  8024  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  suplocexprlemlub  8039  prsrlem1  8057  gt0srpr  8063  caucvgsrlemcl  8104  caucvgsrlembound  8109  caucvgsrlemgt1  8110  suplocsrlemb  8121  suplocsrlem  8123  suplocsr  8124  ltresr  8154  nnindnn  8208  axcaucvglemcl  8210  axcaucvglemval  8212  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  sup3exmid  9231  nnind  9253  nn0supp  9552  nn0ge2m1nn  9560  zleloe  9624  zapne  9652  nn0lt2  9659  suprzclex  9676  zindd  9696  uzm1  9885  uzin  9887  infregelbex  9930  elnn1uz2  9939  nn01to3  9949  divfnzn  9953  qapne  9971  xrltnsym2  10127  xaddass  10202  xleadd1a  10206  xlt2add  10213  xlesubadd  10216  iooval2  10248  icoshftf1o  10324  fztri3or  10373  fzneuz  10435  4fvwrd4  10474  elfzo0  10520  infssuzex  10593  infssuzcldc  10595  suprzubdc  10596  nninfdcex  10597  zsupssdc  10598  exbtwnzlemex  10609  ioom  10620  fzfig  10792  uzennn  10798  uzsinds  10806  iseqovex  10820  seq3val  10822  seqvalcd  10823  seqf  10826  seqovcd  10829  monoord2  10848  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  seq3f1olemqsum  10875  seq3f1o  10879  seqf1og  10883  seq3distr  10894  expp1  10908  expcl2lemap  10913  expclzap  10926  expap0i  10933  nn0ltexp2  11071  bcval5  11125  hashinfuni  11140  hashennnuni  11142  hashnncl  11158  resunimafz0  11198  zfz1isolemiso  11211  zfz1isolem1  11212  zfz1iso  11213  wrdsymb0  11257  wrdlen1  11262  ccat1st1st  11329  swrdrlen  11353  pfxid  11378  pfxwrdsymbg  11382  pfxtrcfv  11385  pfxccat1  11394  pfxpfxid  11401  pfxcctswrd  11402  swrdccatin1  11417  pfxccatin12  11425  pfxccatid  11433  seq3shft  11523  cvg1nlemcau  11669  rexanuz  11673  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  rersqreu  11713  caubnd2  11802  maxleast  11898  fimaxre2  11912  minmax  11915  xrmaxiflemcl  11930  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxadd  11946  xrminmax  11950  xrbdtri  11961  climreu  11982  reccn2ap  11998  iserex  12024  climcvg1nlem  12034  serf0  12037  fz1f1o  12060  summodclem3  12066  zsumdc  12070  fsum3  12073  isumz  12075  isumss  12077  isumss2  12079  fsumsersdc  12081  fsum3ser  12083  fsumsplit  12093  isumclim2  12108  isumclim3  12109  fsum2dlemstep  12120  fsumcnv  12123  fisumcom2  12124  bcxmas  12175  isumle  12181  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratz  12218  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  zproddc  12265  prod1dc  12272  fprodsplitdc  12282  fprodsplit  12283  fprodunsn  12290  fprodcl2lem  12291  fprodcllemf  12299  fprod2dlemstep  12308  fprodcnv  12311  fprodcom2fi  12312  fprodle  12326  ef0lem  12346  fsumdvds  12528  mod2eq1n2dvds  12565  ndvdssub  12616  bitsfzolem  12640  bitsfzo  12641  bitsinv1  12648  gcdsupex  12653  gcdsupcl  12654  bezoutlemnewy  12692  bezoutlemmain  12694  bezoutlembi  12701  bezoutlemeu  12703  bezoutlemle  12704  uzwodc  12733  nnwofdc  12734  nnwosdc  12735  nninfctlemfo  12736  nninfct  12737  nn0seqcvgd  12738  eucalgf  12752  eucalginv  12753  lcmval  12760  prmind2  12817  dfphi2  12917  phiprmpw  12919  phimullem  12922  eulerthlem1  12924  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  eulerth  12930  phisum  12938  odzcllem  12940  odzdvds  12943  pythagtriplem19  12980  pclemub  12985  pcprecl  12987  pceu  12993  pcqmul  13001  pcqcl  13004  pcxnn0cl  13008  pcxqcl  13010  pcge0  13011  pcdvdsb  13018  pceq0  13020  pcneg  13023  pcdvdstr  13025  pcgcd1  13026  pc2dvds  13028  pcz  13030  pcprmpw2  13031  pcaddlem  13037  pcadd  13038  pcmptcl  13040  pcmpt  13041  pcmptdvds  13043  fldivp1  13046  qexpz  13050  pockthlem  13054  pockthg  13055  prmunb  13060  1arith  13065  4sqlemffi  13094  4sqlem17  13105  4sqlem18  13106  4sqlem19  13107  ballotfilem2  13142  ennnfonelemom  13159  ennnfoneleminc  13162  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemdm  13171  ennnfonelemr  13174  ennnfonelemim  13175  exmidunben  13177  ctinfom  13179  inffinp1  13180  ctinf  13181  enctlem  13183  ctiunctlemu1st  13185  ctiunctlemu2nd  13186  ctiunctlemudc  13188  ctiunct  13191  ctiunctal  13192  unct  13193  ssomct  13196  nninfdclemcl  13199  nninfdclemp1  13201  nninfdc  13204  structcnvcnv  13228  setscom  13252  relelbasov  13275  ressbas2d  13281  ressval3d  13285  ressabsg  13289  restid2  13461  imasaddfnlemg  13527  quslem  13537  ercpbl  13544  fnpr2ob  13553  mgmplusf  13579  grpinvalem  13598  grpinva  13599  grprida  13600  fngsum  13601  igsumvalx  13602  gsum0g  13609  gsumval2  13610  ismnd  13632  mhmpropd  13679  grppropd  13730  grpsubf  13792  dfgrp3mlem  13811  mulgnn0p1  13850  mulgnn0subcl  13852  mulgsubcl  13853  mulgneg  13857  mulgnn0dir  13869  mulgnn0ass  13875  submmulg  13883  issubg2m  13906  issubg4m  13910  ghmmulg  13973  ghmrn  13974  lringuplu  14341  rrgsupp  14411  lmodscaf  14458  lssintclm  14532  lspun0  14573  lidlbas  14626  psrbagconcl  14827  psr1clfi  14843  topontopon  14885  eltg3i  14921  epttop  14955  difopn  14973  uncld  14978  0nnei  15018  resttopon  15036  restabs  15040  restopnb  15046  lmcvg  15082  cnptopco  15087  cnss1  15091  cnss2  15092  cncnpi  15093  cncnp2m  15096  cnrest  15100  cnrest2  15101  cnrest2r  15102  cnptoprest  15104  cnptoprest2  15105  lmss  15111  lmff  15114  lmtopcnp  15115  lmcn  15116  txbasval  15132  upxp  15137  txcnmpt  15138  txdis1cn  15143  txlm  15144  lmcn2  15145  cnmpt11  15148  cnmpt11f  15149  cnmpt1t  15150  cnmpt12  15152  cnmpt21  15156  cnmpt21f  15157  cnmpt2t  15158  cnmpt22  15159  cnmpt22f  15160  cnmptcom  15163  hmeocnv  15172  hmeof1o  15174  hmeores  15180  txhmeo  15184  txswaphmeo  15186  isxmet2d  15213  blfvalps  15250  xblss2ps  15269  xblss2  15270  blfps  15274  blf  15275  unirnblps  15287  unirnbl  15288  isxms2  15317  bdxmet  15366  bdmet  15367  xmetxp  15372  xmettx  15375  blssioo  15418  tgioo  15419  mulcncflem  15472  divcncfap  15479  dedekindeulemuub  15482  dedekindeulemub  15483  dedekindeulemloc  15484  dedekindeulemlu  15486  suplociccreex  15489  suplociccex  15490  dedekindicclemuub  15491  dedekindicclemub  15492  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthdich  15518  limcrcl  15523  limcmpted  15528  limccnp2lem  15541  limccnp2cntop  15542  limccoap  15543  dvrecap  15578  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  plyco  15624  plycj  15626  plyrecj  15628  dvply1  15630  dvply2g  15631  cosordlem  15714  logbgcd1irraplemexp  15833  logbgcd1irrap  15835  lgsneg1  15898  lgsdilem  15900  lgsdir2  15906  lgsdirprm  15907  lgsdir  15908  lgsne0  15911  lgsabs1  15912  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1f1o  15933  gausslemma2dlem4  15937  lgseisenlem1  15943  lgsquadlem3  15952  2lgslem1a  15961  2sqlem5  15992  2sqlem7  15994  2sqlem8a  15995  2sqlem8  15996  2sqlem9  15997  gropeld  16044  grstructeld2dom  16045  uhgrm  16073  upgrm  16095  upgr1een  16119  uhgredgm  16131  edgupgren  16136  edgumgren  16137  edgusgren  16158  ausgrusgrben  16163  umgr2edg1  16204  usgredg2vlem1  16217  uhgr0enedgfi  16231  subupgr  16268  vtxedgfi  16284  vtxlpfi  16285  vtxdumgrfival  16293  vtxd0nedgbfi  16294  1hevtxdg0fi  16302  p1evtxdeqfilem  16306  wlkvtxm  16335  g0wlk0  16365  wlkres  16374  trlreslem  16384  clwwlkccatlem  16395  clwwlknnn  16407  trlsegvdeglem6  16460  eupth2lem3lem3fi  16465  eupth2lem3lem7fi  16469  eulerpathum  16476  bj-stand  16520  bj-charfundcALT  16579  bj-charfunbi  16581  bj-bdfindis  16717  bj-peano4  16725  strcollnfALT  16756  pw1map  16769  pwtrufal  16771  pwf1oexmid  16773  subctctexmid  16774  pw1nct  16777  nnsf  16783  nninfalllem1  16786  nninfall  16787  nninfsellemqall  16793  nnnninfen  16799  exmidsbthrlem  16802  sbthom  16806  repiecef  16812  cvgcmp2nlemabs  16816  trilpo  16827  iswomni0  16836  redcwlpo  16840  dceqnconst  16846  dcapnconst  16847  nconstwlpolem  16851  nconstwlpo  16852  neapmkvlem  16853  neapmkv  16854  ltlenmkv  16856  taupi  16859  gfsumval  16862  gsumgfsum  16866  alsi1d  16878  alsi2d  16879  alsc1d  16880  alsc2d  16881