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  2032  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  eu2  2127  2euex  2170  eqcomd  2240  3eltr3g  2319  abbid  2351  neneqd  2435  eqnetrrid  2445  3netr3g  2448  necomd  2500  r19.21bi  2632  nrexdv  2637  rexlimd  2659  rabbidva  2803  elisset  2830  euind  3007  rmoan  3020  reuind  3025  2rmorex  3026  spsbc  3057  spesbc  3132  eldifad  3225  eldifbd  3226  3sstr3g  3284  sseqtrdi  3290  difindiss  3479  un00  3559  undifss  3594  ifcldcd  3664  disjpr2  3758  difprsn1  3838  diftpsn3  3840  difsnss  3845  sneqr  3869  preqr1  3877  preq12b  3879  oprcl  3912  intab  3983  riinm  4069  rintm  4089  disjiun  4109  sndisj  4110  3brtr3g  4147  trint  4228  iinexgm  4271  exmidexmid  4314  exmid01  4316  pwntru  4317  exmid1stab  4326  pwel  4339  exss  4348  0nelop  4369  euotd  4376  opelopabsb  4383  pwunim  4412  issod  4445  frind  4478  suctr  4547  orduniss  4551  onelini  4556  oneluni  4557  eusv2i  4581  rexxfrd  4589  rabxfrd  4595  reuhypd  4597  iunpw  4606  sucexg  4625  ordsucim  4627  ordtriexmidlem  4646  ontriexmidim  4649  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  ordsucunielexmid  4658  orddif  4674  suc11g  4684  onintexmid  4700  reg3exmidlemwe  4706  tfisi  4714  peano1  4721  peano2  4722  finds2  4728  omsinds  4749  brrelex12  4793  brel  4807  ssrel  4843  ssrel2  4845  ssrelrel  4855  elrel  4857  xpsspw  4867  relop  4910  dmxpm  4982  opelresi  5054  mptimass  5119  ndmima  5144  poirr2  5160  xpmlem  5188  xpimasn  5216  iotass  5335  iotacl  5342  dffun5r  5369  funeu  5382  funeu2  5383  funfnd  5388  funopg  5391  funun  5402  fununfun  5404  funinsn  5410  funtp  5414  funcnvuni  5430  funcnvres2  5436  imadiflem  5440  imadif  5441  funimaexglem  5444  fneu2  5468  fnimaeq0  5485  fnmpt  5490  ffrn  5525  fun2  5542  f00  5564  f0bi  5565  fimadmfo  5604  foimacnv  5637  resdif  5641  f1ococnv1  5648  fv3  5698  relelfvdm  5707  elfvm  5708  nfvres  5711  dffn5im  5727  mptfvex  5768  fvmptdf  5770  fvmptdv2  5772  fndmdif  5788  dff4im  5828  fmpt  5832  fmptd  5836  fmptdf  5839  f1oresrab  5847  fcoconst  5853  fsn  5854  funopsn  5865  ftpg  5873  fsnunf  5889  resfunexg  5910  isores1  5993  riota2df  6033  acexmidlemcase  6053  brabvv  6107  funoprabg  6160  fnovim  6170  ovmpodf  6193  ovi3  6199  elmpocl  6257  uchoice  6344  1stcof  6370  2ndcof  6371  opabn1stprc  6402  fnmpo  6411  fmpoco  6425  fo2ndf  6436  f1o2ndf1  6437  disjxp1  6445  fvdifsuppst  6457  fsuppeq  6460  fsuppeqg  6461  suppssrst  6474  suppssrgst  6475  brtpos2  6495  reldmtpos  6497  dftpos3  6506  dftpos4  6507  tpostpos2  6509  tposf2  6512  tposf12  6513  tposfo  6515  tposf  6516  smores2  6538  tfrlem1  6552  tfrlem3-2d  6556  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi1  6576  tfrexlem  6578  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcldm  6607  rdgivallem  6625  rdgisucinc  6629  frecabex  6642  frecfnom  6645  frecfcllem  6648  frecsuclem  6650  omsuc  6718  nntri2  6740  nnsucuniel  6741  nnsseleq  6747  nnm00  6776  ecexr  6785  swoer  6808  elqsn0m  6850  iinerm  6854  erinxp  6856  ecinxp  6857  eroveu  6873  eroprf  6875  mapprc  6899  mapsn  6938  ixpprc  6967  ixp0  6979  resixp  6981  elixpsn  6983  dom2lem  7024  fundmen  7060  1dom1el  7073  dom0  7104  xpf1o  7110  mapxpen  7114  xpmapenlem  7115  ssenen  7118  nneneq  7124  ssfilem  7143  ssfilemd  7145  dif1en  7149  dif1enen  7150  fin0  7155  fin0or  7156  diffitest  7157  diffisn  7163  ac6sfi  7168  fimax2gtrilemstep  7171  fimax2gtri  7172  finexdc  7173  eqsndc  7176  exmidpweq  7182  pw1fin  7183  onunsnss  7190  unsnfidcel  7194  undifdcss  7196  undifdc  7197  tpfidceq  7203  fiintim  7204  fisseneq  7208  fidcenumlemr  7238  sbthlemi4  7243  sbthlemi5  7244  sbthlemi9  7248  fifo  7280  2omap  7282  suplubti  7304  supelti  7306  infmoti  7332  infisoti  7336  djulclb  7359  updjud  7386  omp1eomlem  7398  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumct  7419  nninfninc  7427  nnnninfeq2  7433  finomni  7444  fodjuomnilemdc  7448  fodjum  7450  fodjuomnilemres  7452  fodjumkvlemres  7463  omniwomnimkv  7471  nninfwlporlem  7477  nninfwlpoimlemginf  7480  nninfwlpoim  7483  nninfinfwlpo  7484  ficardon  7498  pr2cv1  7505  exmidonfinlem  7509  en2eleq  7511  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemim  7517  finacn  7524  acfun  7527  exmidaclem  7528  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  pw1if  7548  pw1on  7549  papsym  7576  papcotr  7577  dftap2  7581  2omotaplemst  7588  exmidapne  7590  ccfunen  7594  cc1  7595  cc2lem  7596  cc2  7597  cc3  7598  acnccim  7602  elni2  7645  indpi  7673  distrnqg  7718  subhalfnqq  7745  enq0sym  7763  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  nnnq0lem1  7777  distrnq0  7790  elinp  7805  elnp1st2nd  7807  prltlu  7818  prnmaxl  7819  prnminu  7820  prarloc  7834  nqprm  7873  appdivnq  7894  prmuloc  7897  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemdisj  8005  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemlol  8029  caucvgprprlemexbt  8037  caucvgprprlem1  8040  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  prsrlem1  8073  gt0srpr  8079  caucvgsrlemcl  8120  caucvgsrlembound  8125  caucvgsrlemgt1  8126  suplocsrlemb  8137  suplocsrlem  8139  suplocsr  8140  ltresr  8170  nnindnn  8224  axcaucvglemcl  8226  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  sup3exmid  9248  nnind  9270  nn0supp  9569  nn0ge2m1nn  9577  zleloe  9641  zapne  9669  nn0lt2  9677  suprzclex  9694  zindd  9714  uzm1  9903  uzin  9905  infregelbex  9948  elnn1uz2  9957  nn01to3  9967  divfnzn  9971  qapne  9989  xrltnsym2  10146  xaddass  10221  xleadd1a  10225  xlt2add  10232  xlesubadd  10235  iooval2  10267  icoshftf1o  10343  fztri3or  10393  fzneuz  10457  4fvwrd4  10496  elfzo0  10542  infssuzex  10615  infssuzcldc  10617  infssfzcldc  10618  infssfzledc  10619  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  exbtwnzlemex  10633  ioom  10644  fzfig  10816  uzennn  10822  uzsinds  10830  iseqovex  10844  seq3val  10846  seqvalcd  10847  seqf  10850  seqovcd  10853  monoord2  10872  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1olemqsum  10899  seq3f1o  10903  seqf1og  10907  seq3distr  10918  expp1  10932  expcl2lemap  10937  expclzap  10950  expap0i  10957  nn0ltexp2  11096  bcval5  11150  hashinfuni  11165  hashennnuni  11167  hashnncl  11183  resunimafz0  11223  zfz1isolemiso  11236  zfz1isolem1  11237  zfz1iso  11238  wrdsymb0  11282  wrdlen1  11287  ccat1st1st  11354  swrdrlen  11378  pfxid  11403  pfxwrdsymbg  11407  pfxtrcfv  11410  pfxccat1  11419  pfxpfxid  11426  pfxcctswrd  11427  swrdccatin1  11442  pfxccatin12  11450  pfxccatid  11458  seq3shft  11548  cvg1nlemcau  11694  rexanuz  11698  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  rersqreu  11738  caubnd2  11827  maxleast  11923  fimaxre2  11937  minmax  11940  xrmaxiflemcl  11955  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxadd  11971  xrminmax  11975  xrbdtri  11986  climreu  12007  reccn2ap  12023  iserex  12049  climcvg1nlem  12059  serf0  12062  fz1f1o  12085  summodclem3  12091  zsumdc  12095  fsum3  12098  isumz  12100  isumss  12102  isumss2  12104  fsumsersdc  12106  fsum3ser  12108  fsumsplit  12118  isumclim2  12133  isumclim3  12134  fsum2dlemstep  12145  fsumcnv  12148  fisumcom2  12149  bcxmas  12200  isumle  12206  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  zproddc  12290  prod1dc  12297  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcl2lem  12316  fprodcllemf  12324  fprod2dlemstep  12333  fprodcnv  12336  fprodcom2fi  12337  fprodle  12351  ef0lem  12371  fsumdvds  12553  mod2eq1n2dvds  12590  ndvdssub  12641  bitsfzolem  12665  bitsfzo  12666  bitsinv1  12673  gcdsupex  12678  gcdsupcl  12679  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlembi  12726  bezoutlemeu  12728  bezoutlemle  12729  uzwodc  12758  nnwofdc  12759  nnwosdc  12760  nninfctlemfo  12761  nninfct  12762  nn0seqcvgd  12763  eucalgf  12777  eucalginv  12778  lcmval  12785  prmind2  12842  dfphi2  12942  phiprmpw  12944  phimullem  12947  eulerthlem1  12949  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  eulerth  12955  phisum  12963  odzcllem  12965  odzdvds  12968  pythagtriplem19  13005  pclemub  13010  pcprecl  13012  pceu  13018  pcqmul  13026  pcqcl  13029  pcxnn0cl  13033  pcxqcl  13035  pcge0  13036  pcdvdsb  13043  pceq0  13045  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pc2dvds  13053  pcz  13055  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  pcmptcl  13065  pcmpt  13066  pcmptdvds  13068  fldivp1  13071  qexpz  13075  pockthlem  13079  pockthg  13080  prmunb  13085  1arith  13090  4sqlemffi  13119  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  ballotfilemcdc  13167  ballotfilem2  13172  ballotfilemfp1  13175  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfmpn  13178  ballotfilemefi  13181  ballotfilemiex  13188  ballotfilemro  13210  ennnfonelemom  13243  ennnfoneleminc  13246  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemdm  13255  ennnfonelemr  13258  ennnfonelemim  13259  exmidunben  13261  ctinfom  13263  inffinp1  13264  ctinf  13265  enctlem  13267  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunct  13275  ctiunctal  13276  unct  13277  ssomct  13280  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  structcnvcnv  13312  setscom  13336  relelbasov  13359  ressbas2d  13365  ressval3d  13369  ressabsg  13373  restid2  13545  imasaddfnlemg  13578  quslem  13588  ercpbl  13595  fnpr2ob  13604  mgmplusf  13629  grpinvalem  13648  grpinva  13649  grprida  13650  fngsum  13651  igsumvalx  13652  gsum0g  13659  gsumval2  13660  ismnd  13680  mhmpropd  13721  grppropd  13772  grpsubf  13834  dfgrp3mlem  13853  mulgnn0p1  13886  mulgnn0subcl  13888  mulgsubcl  13889  mulgneg  13893  mulgnn0dir  13905  mulgnn0ass  13911  submmulg  13919  issubg2m  13942  issubg4m  13946  ghmmulg  14009  ghmrn  14010  gfsumval  14102  gsumgfsum  14106  lringuplu  14441  rrgsupp  14512  opprdrng  14558  lmodscaf  14584  lssintclm  14658  lspun0  14699  lidlbas  14752  psrbagconcl  14953  psr1clfi  14969  topontopon  15011  eltg3i  15047  epttop  15081  difopn  15099  uncld  15104  0nnei  15144  resttopon  15162  restabs  15166  restopnb  15172  lmcvg  15208  cnptopco  15213  cnss1  15217  cnss2  15218  cncnpi  15219  cncnp2m  15222  cnrest  15226  cnrest2  15227  cnrest2r  15228  cnptoprest  15230  cnptoprest2  15231  lmss  15237  lmff  15240  lmtopcnp  15241  lmcn  15242  txbasval  15258  upxp  15263  txcnmpt  15264  txdis1cn  15269  txlm  15270  lmcn2  15271  cnmpt11  15274  cnmpt11f  15275  cnmpt1t  15276  cnmpt12  15278  cnmpt21  15282  cnmpt21f  15283  cnmpt2t  15284  cnmpt22  15285  cnmpt22f  15286  cnmptcom  15289  hmeocnv  15298  hmeof1o  15300  hmeores  15306  txhmeo  15310  txswaphmeo  15312  isxmet2d  15339  blfvalps  15376  xblss2ps  15395  xblss2  15396  blfps  15400  blf  15401  unirnblps  15413  unirnbl  15414  isxms2  15443  bdxmet  15492  bdmet  15493  xmetxp  15498  xmettx  15501  blssioo  15544  tgioo  15545  mulcncflem  15598  divcncfap  15605  dedekindeulemuub  15608  dedekindeulemub  15609  dedekindeulemloc  15610  dedekindeulemlu  15612  suplociccreex  15615  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemub  15618  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthdich  15644  limcrcl  15649  limcmpted  15654  limccnp2lem  15667  limccnp2cntop  15668  limccoap  15669  dvrecap  15704  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plyco  15750  plycj  15752  plyrecj  15754  dvply1  15756  dvply2g  15757  cosordlem  15840  logbgcd1irraplemexp  15959  logbgcd1irrap  15961  lgsneg1  16024  lgsdilem  16026  lgsdir2  16032  lgsdirprm  16033  lgsdir  16034  lgsne0  16037  lgsabs1  16038  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1f1o  16059  gausslemma2dlem4  16063  lgseisenlem1  16069  lgsquadlem3  16078  2lgslem1a  16087  2sqlem5  16118  2sqlem7  16120  2sqlem8a  16121  2sqlem8  16122  2sqlem9  16123  gropeld  16170  grstructeld2dom  16171  uhgrm  16199  upgrm  16221  upgr1een  16245  uhgredgm  16257  edgupgren  16262  edgumgren  16263  edgusgren  16284  ausgrusgrben  16289  umgr2edg1  16330  usgredg2vlem1  16343  uhgr0enedgfi  16357  subupgr  16394  vtxedgfi  16410  vtxlpfi  16411  vtxdumgrfival  16419  vtxd0nedgbfi  16420  1hevtxdg0fi  16428  p1evtxdeqfilem  16432  wlkvtxm  16461  g0wlk0  16491  wlkres  16500  trlreslem  16510  clwwlkccatlem  16521  clwwlknnn  16533  trlsegvdeglem6  16586  eupth2lem3lem3fi  16591  eupth2lem3lem7fi  16595  eulerpathum  16602  bj-stand  16646  bj-charfundcALT  16705  bj-charfunbi  16707  bj-bdfindis  16843  bj-peano4  16851  strcollnfALT  16882  pw1map  16895  pwtrufal  16897  pwf1oexmid  16899  subctctexmid  16900  pw1nct  16903  nnsf  16909  nninfalllem1  16912  nninfall  16913  nninfsellemqall  16919  nnnninfen  16925  exmidsbthrlem  16928  sbthom  16932  repiecef  16938  cvgcmp2nlemabs  16942  trilpo  16953  iswomni0  16962  redcwlpo  16966  dceqnconst  16972  dcapnconst  16973  nconstwlpolem  16977  nconstwlpo  16978  neapmkvlem  16979  neapmkv  16980  ltlenmkv  16982  taupi  16985  alsi1d  16993  alsi2d  16994  alsc1d  16995  alsc2d  16996