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  444  orcomd  719  3mix3  1153  mpjao3dan  1286  ecase23d  1329  exlimdh  1576  nexd  1593  alexnim  1628  excomim  1642  19.41  1665  equcomd  1684  nfexd  1735  sbh  1750  sbcof2  1783  sbidm  1824  sb6rf  1826  nfsbt  1950  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  eu2  2044  2euex  2087  eqcomd  2146  3eltr3g  2225  abbid  2257  neneqd  2330  eqnetrrid  2340  3netr3g  2343  necomd  2395  r19.21bi  2523  nrexdv  2528  rexlimd  2549  rabbidva  2677  elisset  2703  euind  2875  rmoan  2888  reuind  2893  2rmorex  2894  spsbc  2924  spesbc  2998  eldifad  3087  eldifbd  3088  3sstr3g  3144  sseqtrdi  3150  difindiss  3335  un00  3414  undifss  3448  ifcldcd  3512  disjpr2  3595  difprsn1  3667  diftpsn3  3669  difsnss  3674  sneqr  3695  preqr1  3703  preq12b  3705  oprcl  3737  intab  3808  riinm  3893  rintm  3913  disjiun  3932  sndisj  3933  3brtr3g  3969  trint  4049  iinexgm  4087  exmidexmid  4128  exmid01  4129  pwntru  4130  pwel  4148  exss  4157  0nelop  4178  euotd  4184  opelopabsb  4190  pwunim  4216  issod  4249  frind  4282  suctr  4351  orduniss  4355  onelini  4360  oneluni  4361  eusv2i  4384  rexxfrd  4392  rabxfrd  4398  reuhypd  4400  iunpw  4409  sucexg  4422  ordsucim  4424  ordtriexmidlem  4443  ordtri2or2exmidlem  4449  onsucelsucexmidlem  4452  ordsucunielexmid  4454  orddif  4470  suc11g  4480  onintexmid  4495  reg3exmidlemwe  4501  tfisi  4509  peano1  4516  peano2  4517  finds2  4523  omsinds  4543  brrelex12  4585  brel  4599  ssrel  4635  ssrel2  4637  ssrelrel  4647  elrel  4649  xpsspw  4659  relop  4697  dmxpm  4767  opelresi  4838  ndmima  4924  poirr2  4939  xpmlem  4967  xpimasn  4995  iotass  5113  iotacl  5119  dffun5r  5143  funeu  5156  funeu2  5157  funfnd  5162  funopg  5165  funun  5175  funinsn  5180  funtp  5184  funcnvuni  5200  funcnvres2  5206  imadiflem  5210  imadif  5211  funimaexglem  5214  fneu2  5236  fnimaeq0  5252  fnmpt  5257  fun2  5304  f00  5322  f0bi  5323  foimacnv  5393  resdif  5397  f1ococnv1  5404  fv3  5452  relelfvdm  5461  nfvres  5462  dffn5im  5475  mptfvex  5514  fvmptdf  5516  fvmptdv2  5518  fndmdif  5533  dff4im  5574  fmpt  5578  fmptd  5582  fmptdf  5585  f1oresrab  5593  fcoconst  5599  fsn  5600  ftpg  5612  fsnunf  5628  resfunexg  5649  isores1  5723  riota2df  5758  acexmidlemcase  5777  brabvv  5825  funoprabg  5878  fnovim  5887  ovmpodf  5910  ovi3  5915  grprinvlem  5973  grprinvd  5974  grpridd  5975  elmpocl  5976  1stcof  6069  2ndcof  6070  fnmpo  6108  fmpoco  6121  fo2ndf  6132  f1o2ndf1  6133  disjxp1  6141  brtpos2  6156  reldmtpos  6158  dftpos3  6167  dftpos4  6168  tpostpos2  6170  tposf2  6173  tposf12  6174  tposfo  6176  tposf  6177  smores2  6199  tfrlem1  6213  tfrlem3-2d  6217  tfrlemisucaccv  6230  tfrlemibxssdm  6232  tfrlemibfn  6233  tfrlemi1  6237  tfrexlem  6239  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcldm  6268  rdgivallem  6286  rdgisucinc  6290  frecabex  6303  frecfnom  6306  frecfcllem  6309  frecsuclem  6311  omsuc  6376  nntri2  6398  nnsucuniel  6399  nnsseleq  6405  nnm00  6433  ecexr  6442  swoer  6465  elqsn0m  6505  iinerm  6509  erinxp  6511  ecinxp  6512  eroveu  6528  eroprf  6530  mapprc  6554  mapsn  6592  ixpprc  6621  ixp0  6633  resixp  6635  elixpsn  6637  dom2lem  6674  fundmen  6708  dom0  6740  xpf1o  6746  mapxpen  6750  xpmapenlem  6751  ssenen  6753  nneneq  6759  ssfilem  6777  dif1en  6781  dif1enen  6782  fin0  6787  fin0or  6788  diffitest  6789  diffisn  6795  ac6sfi  6800  fimax2gtrilemstep  6802  fimax2gtri  6803  finexdc  6804  onunsnss  6813  unsnfidcel  6817  undifdcss  6819  undifdc  6820  fiintim  6825  fisseneq  6828  fidcenumlemr  6851  sbthlemi4  6856  sbthlemi5  6857  sbthlemi9  6861  fifo  6876  suplubti  6895  supelti  6897  infmoti  6923  infisoti  6927  djulclb  6948  updjud  6975  omp1eomlem  6987  0ct  7000  ctmlemr  7001  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumct  7008  finomni  7020  fodjuomnilemdc  7024  fodjum  7026  fodjuomnilemres  7028  fodjumkvlemres  7041  omniwomnimkv  7049  exmidonfinlem  7066  en2eleq  7068  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemim  7074  acfun  7080  exmidaclem  7081  ccfunen  7096  cc1  7097  cc2lem  7098  cc2  7099  cc3  7100  elni2  7146  indpi  7174  distrnqg  7219  subhalfnqq  7246  enq0sym  7264  enq0ref  7265  enq0tr  7266  nqnq0pi  7270  nnnq0lem1  7278  distrnq0  7291  elinp  7306  elnp1st2nd  7308  prltlu  7319  prnmaxl  7320  prnminu  7321  prarloc  7335  nqprm  7374  appdivnq  7395  prmuloc  7398  mullocpr  7403  distrlem4prl  7416  distrlem4pru  7417  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemopu  7435  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlemdisj  7483  cauappcvgprlem2  7492  cauappcvgprlemlim  7493  caucvgprlemnkj  7498  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlemdisj  7506  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem2  7512  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemlol  7530  caucvgprprlemexbt  7538  caucvgprprlem1  7541  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  prsrlem1  7574  gt0srpr  7580  caucvgsrlemcl  7621  caucvgsrlembound  7626  caucvgsrlemgt1  7627  suplocsrlemb  7638  suplocsrlem  7640  suplocsr  7641  ltresr  7671  nnindnn  7725  axcaucvglemcl  7727  axcaucvglemval  7729  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  sup3exmid  8739  nnind  8760  nn0supp  9053  nn0ge2m1nn  9061  zleloe  9125  zapne  9149  nn0lt2  9156  suprzclex  9173  zindd  9193  uzm1  9380  uzin  9382  elnn1uz2  9428  nn01to3  9436  divfnzn  9440  qapne  9458  xrltnsym2  9610  xaddass  9682  xleadd1a  9686  xlt2add  9693  xlesubadd  9696  iooval2  9728  icoshftf1o  9804  fztri3or  9850  fzneuz  9912  4fvwrd4  9948  elfzo0  9990  exbtwnzlemex  10058  ioom  10069  fzfig  10234  uzennn  10240  uzsinds  10246  iseqovex  10260  seq3val  10262  seqvalcd  10263  seqf  10265  seqovcd  10267  monoord2  10281  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  seq3f1olemqsum  10304  seq3f1o  10308  seq3distr  10317  expp1  10331  expcl2lemap  10336  expclzap  10349  expap0i  10356  bcval5  10541  hashinfuni  10555  hashennnuni  10557  hashnncl  10574  resunimafz0  10606  zfz1isolemiso  10614  zfz1isolem1  10615  zfz1iso  10616  seq3shft  10642  cvg1nlemcau  10788  rexanuz  10792  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  rersqreu  10832  caubnd2  10921  maxleast  11017  fimaxre2  11030  minmax  11033  xrmaxiflemcl  11046  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxadd  11062  xrminmax  11066  xrbdtri  11077  climreu  11098  reccn2ap  11114  iserex  11140  climcvg1nlem  11150  serf0  11153  fz1f1o  11176  summodclem3  11181  zsumdc  11185  fsum3  11188  isumz  11190  isumss  11192  isumss2  11194  fsumsersdc  11196  fsum3ser  11198  fsumsplit  11208  isumclim2  11223  isumclim3  11224  fsum2dlemstep  11235  fsumcnv  11238  fisumcom2  11239  bcxmas  11290  isumle  11296  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratz  11333  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  zproddc  11380  ef0lem  11403  mod2eq1n2dvds  11612  ndvdssub  11663  infssuzex  11678  infssuzcldc  11680  gcdsupex  11682  gcdsupcl  11683  bezoutlemnewy  11720  bezoutlemmain  11722  bezoutlembi  11729  bezoutlemeu  11731  bezoutlemle  11732  nn0seqcvgd  11758  eucalgf  11772  eucalginv  11773  lcmval  11780  prmind2  11837  dfphi2  11932  phiprmpw  11934  phimullem  11937  ennnfonelemom  11957  ennnfoneleminc  11960  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemdm  11969  ennnfonelemr  11972  ennnfonelemim  11973  exmidunben  11975  ctinfom  11977  inffinp1  11978  ctinf  11979  enctlem  11981  ctiunctlemu1st  11983  ctiunctlemu2nd  11984  ctiunctlemudc  11986  ctiunct  11989  ctiunctal  11990  unct  11991  structcnvcnv  12014  setscom  12038  restid2  12168  topontopon  12226  eltg3i  12264  epttop  12298  difopn  12316  uncld  12321  0nnei  12361  resttopon  12379  restabs  12383  restopnb  12389  lmcvg  12425  cnptopco  12430  cnss1  12434  cnss2  12435  cncnpi  12436  cncnp2m  12439  cnrest  12443  cnrest2  12444  cnrest2r  12445  cnptoprest  12447  cnptoprest2  12448  lmss  12454  lmff  12457  lmtopcnp  12458  lmcn  12459  txbasval  12475  upxp  12480  txcnmpt  12481  txdis1cn  12486  txlm  12487  lmcn2  12488  cnmpt11  12491  cnmpt11f  12492  cnmpt1t  12493  cnmpt12  12495  cnmpt21  12499  cnmpt21f  12500  cnmpt2t  12501  cnmpt22  12502  cnmpt22f  12503  cnmptcom  12506  hmeocnv  12515  hmeof1o  12517  hmeores  12523  txhmeo  12527  txswaphmeo  12529  isxmet2d  12556  blfvalps  12593  xblss2ps  12612  xblss2  12613  blfps  12617  blf  12618  unirnblps  12630  unirnbl  12631  isxms2  12660  bdxmet  12709  bdmet  12710  xmetxp  12715  xmettx  12718  blssioo  12753  tgioo  12754  mulcncflem  12798  dedekindeulemuub  12803  dedekindeulemub  12804  dedekindeulemloc  12805  dedekindeulemlu  12807  suplociccreex  12810  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemub  12813  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemuopn  12824  limcrcl  12835  limcmpted  12840  limccnp2lem  12853  limccnp2cntop  12854  limccoap  12855  dvrecap  12885  cosordlem  12978  logbgcd1irraplemexp  13093  logbgcd1irrap  13095  bj-stand  13127  bj-bdfindis  13316  bj-peano4  13324  strcollnfALT  13355  pwtrufal  13365  pwf1oexmid  13367  exmid1stab  13368  subctctexmid  13369  pw1nct  13371  nnsf  13374  nninfalllem1  13378  nninfall  13379  nninfsellemqall  13386  exmidsbthrlem  13392  sbthom  13396  cvgcmp2nlemabs  13402  trilpo  13411  redcwlpo  13422  dceqnconst  13423  neapmkvlem  13424  neapmkv  13425  taupi  13430  alsi1d  13438  alsi2d  13439  alsc1d  13440  alsc2d  13441