Theorem sylib 121

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 119	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb1  136  bicomd  140  pm5.74d  181  bitri  183  3imtr3i  199  ancomd  265  pm4.71d  391  pm4.71rd  392  imdistand  445  orcomd  724  3mix3  1163  mpjao3dan  1302  ecase23d  1345  exlimdh  1589  nexd  1606  alexnim  1641  excomim  1656  19.41  1679  equcomd  1700  nfexd  1754  sbh  1769  sbcof2  1803  sbidm  1844  sb6rf  1846  nfsbt  1969  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  eu2  2063  2euex  2106  eqcomd  2176  3eltr3g  2255  abbid  2287  neneqd  2361  eqnetrrid  2371  3netr3g  2374  necomd  2426  r19.21bi  2558  nrexdv  2563  rexlimd  2584  rabbidva  2718  elisset  2744  euind  2917  rmoan  2930  reuind  2935  2rmorex  2936  spsbc  2966  spesbc  3040  eldifad  3132  eldifbd  3133  3sstr3g  3189  sseqtrdi  3195  difindiss  3381  un00  3461  undifss  3495  ifcldcd  3561  disjpr2  3647  difprsn1  3719  diftpsn3  3721  difsnss  3726  sneqr  3747  preqr1  3755  preq12b  3757  oprcl  3789  intab  3860  riinm  3945  rintm  3965  disjiun  3984  sndisj  3985  3brtr3g  4022  trint  4102  iinexgm  4140  exmidexmid  4182  exmid01  4184  pwntru  4185  pwel  4203  exss  4212  0nelop  4233  euotd  4239  opelopabsb  4245  pwunim  4271  issod  4304  frind  4337  suctr  4406  orduniss  4410  onelini  4415  oneluni  4416  eusv2i  4440  rexxfrd  4448  rabxfrd  4454  reuhypd  4456  iunpw  4465  sucexg  4482  ordsucim  4484  ordtriexmidlem  4503  ontriexmidim  4506  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  ordsucunielexmid  4515  orddif  4531  suc11g  4541  onintexmid  4557  reg3exmidlemwe  4563  tfisi  4571  peano1  4578  peano2  4579  finds2  4585  omsinds  4606  brrelex12  4649  brel  4663  ssrel  4699  ssrel2  4701  ssrelrel  4711  elrel  4713  xpsspw  4723  relop  4761  dmxpm  4831  opelresi  4902  ndmima  4988  poirr2  5003  xpmlem  5031  xpimasn  5059  iotass  5177  iotacl  5183  dffun5r  5210  funeu  5223  funeu2  5224  funfnd  5229  funopg  5232  funun  5242  funinsn  5247  funtp  5251  funcnvuni  5267  funcnvres2  5273  imadiflem  5277  imadif  5278  funimaexglem  5281  fneu2  5303  fnimaeq0  5319  fnmpt  5324  fun2  5371  f00  5389  f0bi  5390  foimacnv  5460  resdif  5464  f1ococnv1  5471  fv3  5519  relelfvdm  5528  nfvres  5529  dffn5im  5542  mptfvex  5581  fvmptdf  5583  fvmptdv2  5585  fndmdif  5601  dff4im  5642  fmpt  5646  fmptd  5650  fmptdf  5653  f1oresrab  5661  fcoconst  5667  fsn  5668  ftpg  5680  fsnunf  5696  resfunexg  5717  isores1  5793  riota2df  5829  acexmidlemcase  5848  brabvv  5899  funoprabg  5952  fnovim  5961  ovmpodf  5984  ovi3  5989  elmpocl  6047  1stcof  6142  2ndcof  6143  fnmpo  6181  fmpoco  6195  fo2ndf  6206  f1o2ndf1  6207  disjxp1  6215  brtpos2  6230  reldmtpos  6232  dftpos3  6241  dftpos4  6242  tpostpos2  6244  tposf2  6247  tposf12  6248  tposfo  6250  tposf  6251  smores2  6273  tfrlem1  6287  tfrlem3-2d  6291  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrlemi1  6311  tfrexlem  6313  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcldm  6342  rdgivallem  6360  rdgisucinc  6364  frecabex  6377  frecfnom  6380  frecfcllem  6383  frecsuclem  6385  omsuc  6451  nntri2  6473  nnsucuniel  6474  nnsseleq  6480  nnm00  6509  ecexr  6518  swoer  6541  elqsn0m  6581  iinerm  6585  erinxp  6587  ecinxp  6588  eroveu  6604  eroprf  6606  mapprc  6630  mapsn  6668  ixpprc  6697  ixp0  6709  resixp  6711  elixpsn  6713  dom2lem  6750  fundmen  6784  dom0  6816  xpf1o  6822  mapxpen  6826  xpmapenlem  6827  ssenen  6829  nneneq  6835  ssfilem  6853  dif1en  6857  dif1enen  6858  fin0  6863  fin0or  6864  diffitest  6865  diffisn  6871  ac6sfi  6876  fimax2gtrilemstep  6878  fimax2gtri  6879  finexdc  6880  exmidpweq  6887  pw1fin  6888  onunsnss  6894  unsnfidcel  6898  undifdcss  6900  undifdc  6901  fiintim  6906  fisseneq  6909  fidcenumlemr  6932  sbthlemi4  6937  sbthlemi5  6938  sbthlemi9  6942  fifo  6957  suplubti  6977  supelti  6979  infmoti  7005  infisoti  7009  djulclb  7032  updjud  7059  omp1eomlem  7071  0ct  7084  ctmlemr  7085  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  enumct  7092  nnnninfeq2  7105  finomni  7116  fodjuomnilemdc  7120  fodjum  7122  fodjuomnilemres  7124  fodjumkvlemres  7135  omniwomnimkv  7143  nninfwlporlem  7149  nninfwlpoimlemginf  7152  nninfwlpoim  7154  exmidonfinlem  7170  en2eleq  7172  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  exmidfodomrlemim  7178  acfun  7184  exmidaclem  7185  exmidontriimlem3  7200  exmidontriimlem4  7201  exmidontriim  7202  pw1on  7203  ccfunen  7226  cc1  7227  cc2lem  7228  cc2  7229  cc3  7230  elni2  7276  indpi  7304  distrnqg  7349  subhalfnqq  7376  enq0sym  7394  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nnnq0lem1  7408  distrnq0  7421  elinp  7436  elnp1st2nd  7438  prltlu  7449  prnmaxl  7450  prnminu  7451  prarloc  7465  nqprm  7504  appdivnq  7525  prmuloc  7528  mullocpr  7533  distrlem4prl  7546  distrlem4pru  7547  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  cauappcvgprlemopl  7608  cauappcvgprlemopu  7610  cauappcvgprlemdisj  7613  cauappcvgprlem2  7622  cauappcvgprlemlim  7623  caucvgprlemnkj  7628  caucvgprlemopl  7631  caucvgprlemopu  7633  caucvgprlemdisj  7636  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem2  7642  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemlol  7660  caucvgprprlemexbt  7668  caucvgprprlem1  7671  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  prsrlem1  7704  gt0srpr  7710  caucvgsrlemcl  7751  caucvgsrlembound  7756  caucvgsrlemgt1  7757  suplocsrlemb  7768  suplocsrlem  7770  suplocsr  7771  ltresr  7801  nnindnn  7855  axcaucvglemcl  7857  axcaucvglemval  7859  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  sup3exmid  8873  nnind  8894  nn0supp  9187  nn0ge2m1nn  9195  zleloe  9259  zapne  9286  nn0lt2  9293  suprzclex  9310  zindd  9330  uzm1  9517  uzin  9519  infregelbex  9557  elnn1uz2  9566  nn01to3  9576  divfnzn  9580  qapne  9598  xrltnsym2  9751  xaddass  9826  xleadd1a  9830  xlt2add  9837  xlesubadd  9840  iooval2  9872  icoshftf1o  9948  fztri3or  9995  fzneuz  10057  4fvwrd4  10096  elfzo0  10138  exbtwnzlemex  10206  ioom  10217  fzfig  10386  uzennn  10392  uzsinds  10398  iseqovex  10412  seq3val  10414  seqvalcd  10415  seqf  10417  seqovcd  10419  monoord2  10433  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  seq3f1olemqsum  10456  seq3f1o  10460  seq3distr  10469  expp1  10483  expcl2lemap  10488  expclzap  10501  expap0i  10508  nn0ltexp2  10644  bcval5  10697  hashinfuni  10711  hashennnuni  10713  hashnncl  10730  resunimafz0  10766  zfz1isolemiso  10774  zfz1isolem1  10775  zfz1iso  10776  seq3shft  10802  cvg1nlemcau  10948  rexanuz  10952  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  rersqreu  10992  caubnd2  11081  maxleast  11177  fimaxre2  11190  minmax  11193  xrmaxiflemcl  11208  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxadd  11224  xrminmax  11228  xrbdtri  11239  climreu  11260  reccn2ap  11276  iserex  11302  climcvg1nlem  11312  serf0  11315  fz1f1o  11338  summodclem3  11343  zsumdc  11347  fsum3  11350  isumz  11352  isumss  11354  isumss2  11356  fsumsersdc  11358  fsum3ser  11360  fsumsplit  11370  isumclim2  11385  isumclim3  11386  fsum2dlemstep  11397  fsumcnv  11400  fisumcom2  11401  bcxmas  11452  isumle  11458  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratz  11495  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  zproddc  11542  prod1dc  11549  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  fprodcl2lem  11568  fprodcllemf  11576  fprod2dlemstep  11585  fprodcnv  11588  fprodcom2fi  11589  fprodle  11603  ef0lem  11623  mod2eq1n2dvds  11838  ndvdssub  11889  infssuzex  11904  infssuzcldc  11906  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  gcdsupex  11912  gcdsupcl  11913  bezoutlemnewy  11951  bezoutlemmain  11953  bezoutlembi  11960  bezoutlemeu  11962  bezoutlemle  11963  uzwodc  11992  nnwofdc  11993  nnwosdc  11994  nn0seqcvgd  11995  eucalgf  12009  eucalginv  12010  lcmval  12017  prmind2  12074  dfphi2  12174  phiprmpw  12176  phimullem  12179  eulerthlem1  12181  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  eulerth  12187  phisum  12194  odzcllem  12196  odzdvds  12199  pythagtriplem19  12236  pclemub  12241  pcprecl  12243  pceu  12249  pcqmul  12257  pcqcl  12260  pcxnn0cl  12264  pcge0  12266  pcdvdsb  12273  pceq0  12275  pcneg  12278  pcdvdstr  12280  pcgcd1  12281  pc2dvds  12283  pcz  12285  pcprmpw2  12286  pcaddlem  12292  pcadd  12293  pcmptcl  12294  pcmpt  12295  pcmptdvds  12297  fldivp1  12300  qexpz  12304  pockthlem  12308  pockthg  12309  prmunb  12314  1arith  12319  ennnfonelemom  12363  ennnfoneleminc  12366  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemdm  12375  ennnfonelemr  12378  ennnfonelemim  12379  exmidunben  12381  ctinfom  12383  inffinp1  12384  ctinf  12385  enctlem  12387  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunct  12395  ctiunctal  12396  unct  12397  ssomct  12400  nninfdclemcl  12403  nninfdclemp1  12405  nninfdc  12408  structcnvcnv  12432  setscom  12456  restid2  12588  mgmplusf  12620  grprinvlem  12639  grprinvd  12640  grpridd  12641  ismnd  12655  mhmpropd  12689  grppropd  12724  topontopon  12812  eltg3i  12850  epttop  12884  difopn  12902  uncld  12907  0nnei  12947  resttopon  12965  restabs  12969  restopnb  12975  lmcvg  13011  cnptopco  13016  cnss1  13020  cnss2  13021  cncnpi  13022  cncnp2m  13025  cnrest  13029  cnrest2  13030  cnrest2r  13031  cnptoprest  13033  cnptoprest2  13034  lmss  13040  lmff  13043  lmtopcnp  13044  lmcn  13045  txbasval  13061  upxp  13066  txcnmpt  13067  txdis1cn  13072  txlm  13073  lmcn2  13074  cnmpt11  13077  cnmpt11f  13078  cnmpt1t  13079  cnmpt12  13081  cnmpt21  13085  cnmpt21f  13086  cnmpt2t  13087  cnmpt22  13088  cnmpt22f  13089  cnmptcom  13092  hmeocnv  13101  hmeof1o  13103  hmeores  13109  txhmeo  13113  txswaphmeo  13115  isxmet2d  13142  blfvalps  13179  xblss2ps  13198  xblss2  13199  blfps  13203  blf  13204  unirnblps  13216  unirnbl  13217  isxms2  13246  bdxmet  13295  bdmet  13296  xmetxp  13301  xmettx  13304  blssioo  13339  tgioo  13340  mulcncflem  13384  dedekindeulemuub  13389  dedekindeulemub  13390  dedekindeulemloc  13391  dedekindeulemlu  13393  suplociccreex  13396  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemub  13399  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemuopn  13410  limcrcl  13421  limcmpted  13426  limccnp2lem  13439  limccnp2cntop  13440  limccoap  13441  dvrecap  13471  cosordlem  13564  logbgcd1irraplemexp  13680  logbgcd1irrap  13682  lgsneg1  13720  lgsdilem  13722  lgsdir2  13728  lgsdirprm  13729  lgsdir  13730  lgsne0  13733  lgsabs1  13734  lgsdirnn0  13742  lgsdinn0  13743  2sqlem5  13749  2sqlem7  13751  2sqlem8a  13752  2sqlem8  13753  2sqlem9  13754  bj-stand  13783  bj-charfundcALT  13844  bj-charfunbi  13846  bj-bdfindis  13982  bj-peano4  13990  strcollnfALT  14021  pwtrufal  14030  pwf1oexmid  14032  exmid1stab  14033  subctctexmid  14034  pw1nct  14036  nnsf  14038  nninfalllem1  14041  nninfall  14042  nninfsellemqall  14048  exmidsbthrlem  14054  sbthom  14058  cvgcmp2nlemabs  14064  trilpo  14075  iswomni0  14083  redcwlpo  14087  dceqnconst  14091  dcapnconst  14092  nconstwlpolem  14096  nconstwlpo  14097  neapmkvlem  14098  neapmkv  14099  taupi  14102  alsi1d  14110  alsi2d  14111  alsc1d  14112  alsc2d  14113