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  1158  mpjao3dan  1297  ecase23d  1340  exlimdh  1584  nexd  1601  alexnim  1636  excomim  1651  19.41  1674  equcomd  1695  nfexd  1749  sbh  1764  sbcof2  1798  sbidm  1839  sb6rf  1841  nfsbt  1964  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  eu2  2058  2euex  2101  eqcomd  2171  3eltr3g  2250  abbid  2282  neneqd  2356  eqnetrrid  2366  3netr3g  2369  necomd  2421  r19.21bi  2553  nrexdv  2558  rexlimd  2579  rabbidva  2713  elisset  2739  euind  2912  rmoan  2925  reuind  2930  2rmorex  2931  spsbc  2961  spesbc  3035  eldifad  3126  eldifbd  3127  3sstr3g  3183  sseqtrdi  3189  difindiss  3375  un00  3454  undifss  3488  ifcldcd  3554  disjpr2  3639  difprsn1  3711  diftpsn3  3713  difsnss  3718  sneqr  3739  preqr1  3747  preq12b  3749  oprcl  3781  intab  3852  riinm  3937  rintm  3957  disjiun  3976  sndisj  3977  3brtr3g  4014  trint  4094  iinexgm  4132  exmidexmid  4174  exmid01  4176  pwntru  4177  pwel  4195  exss  4204  0nelop  4225  euotd  4231  opelopabsb  4237  pwunim  4263  issod  4296  frind  4329  suctr  4398  orduniss  4402  onelini  4407  oneluni  4408  eusv2i  4432  rexxfrd  4440  rabxfrd  4446  reuhypd  4448  iunpw  4457  sucexg  4474  ordsucim  4476  ordtriexmidlem  4495  ontriexmidim  4498  ordtri2or2exmidlem  4502  onsucelsucexmidlem  4505  ordsucunielexmid  4507  orddif  4523  suc11g  4533  onintexmid  4549  reg3exmidlemwe  4555  tfisi  4563  peano1  4570  peano2  4571  finds2  4577  omsinds  4598  brrelex12  4641  brel  4655  ssrel  4691  ssrel2  4693  ssrelrel  4703  elrel  4705  xpsspw  4715  relop  4753  dmxpm  4823  opelresi  4894  ndmima  4980  poirr2  4995  xpmlem  5023  xpimasn  5051  iotass  5169  iotacl  5175  dffun5r  5199  funeu  5212  funeu2  5213  funfnd  5218  funopg  5221  funun  5231  funinsn  5236  funtp  5240  funcnvuni  5256  funcnvres2  5262  imadiflem  5266  imadif  5267  funimaexglem  5270  fneu2  5292  fnimaeq0  5308  fnmpt  5313  fun2  5360  f00  5378  f0bi  5379  foimacnv  5449  resdif  5453  f1ococnv1  5460  fv3  5508  relelfvdm  5517  nfvres  5518  dffn5im  5531  mptfvex  5570  fvmptdf  5572  fvmptdv2  5574  fndmdif  5589  dff4im  5630  fmpt  5634  fmptd  5638  fmptdf  5641  f1oresrab  5649  fcoconst  5655  fsn  5656  ftpg  5668  fsnunf  5684  resfunexg  5705  isores1  5781  riota2df  5817  acexmidlemcase  5836  brabvv  5884  funoprabg  5937  fnovim  5946  ovmpodf  5969  ovi3  5974  grprinvlem  6032  grprinvd  6033  grpridd  6034  elmpocl  6035  1stcof  6128  2ndcof  6129  fnmpo  6167  fmpoco  6180  fo2ndf  6191  f1o2ndf1  6192  disjxp1  6200  brtpos2  6215  reldmtpos  6217  dftpos3  6226  dftpos4  6227  tpostpos2  6229  tposf2  6232  tposf12  6233  tposfo  6235  tposf  6236  smores2  6258  tfrlem1  6272  tfrlem3-2d  6276  tfrlemisucaccv  6289  tfrlemibxssdm  6291  tfrlemibfn  6292  tfrlemi1  6296  tfrexlem  6298  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemaccex  6312  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemaccex  6325  tfrcldm  6327  rdgivallem  6345  rdgisucinc  6349  frecabex  6362  frecfnom  6365  frecfcllem  6368  frecsuclem  6370  omsuc  6436  nntri2  6458  nnsucuniel  6459  nnsseleq  6465  nnm00  6493  ecexr  6502  swoer  6525  elqsn0m  6565  iinerm  6569  erinxp  6571  ecinxp  6572  eroveu  6588  eroprf  6590  mapprc  6614  mapsn  6652  ixpprc  6681  ixp0  6693  resixp  6695  elixpsn  6697  dom2lem  6734  fundmen  6768  dom0  6800  xpf1o  6806  mapxpen  6810  xpmapenlem  6811  ssenen  6813  nneneq  6819  ssfilem  6837  dif1en  6841  dif1enen  6842  fin0  6847  fin0or  6848  diffitest  6849  diffisn  6855  ac6sfi  6860  fimax2gtrilemstep  6862  fimax2gtri  6863  finexdc  6864  exmidpweq  6871  pw1fin  6872  onunsnss  6878  unsnfidcel  6882  undifdcss  6884  undifdc  6885  fiintim  6890  fisseneq  6893  fidcenumlemr  6916  sbthlemi4  6921  sbthlemi5  6922  sbthlemi9  6926  fifo  6941  suplubti  6961  supelti  6963  infmoti  6989  infisoti  6993  djulclb  7016  updjud  7043  omp1eomlem  7055  0ct  7068  ctmlemr  7069  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  enumct  7076  nnnninfeq2  7089  finomni  7100  fodjuomnilemdc  7104  fodjum  7106  fodjuomnilemres  7108  fodjumkvlemres  7119  omniwomnimkv  7127  exmidonfinlem  7145  en2eleq  7147  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  exmidfodomrlemim  7153  acfun  7159  exmidaclem  7160  exmidontriimlem3  7175  exmidontriimlem4  7176  exmidontriim  7177  pw1on  7178  ccfunen  7201  cc1  7202  cc2lem  7203  cc2  7204  cc3  7205  elni2  7251  indpi  7279  distrnqg  7324  subhalfnqq  7351  enq0sym  7369  enq0ref  7370  enq0tr  7371  nqnq0pi  7375  nnnq0lem1  7383  distrnq0  7396  elinp  7411  elnp1st2nd  7413  prltlu  7424  prnmaxl  7425  prnminu  7426  prarloc  7440  nqprm  7479  appdivnq  7500  prmuloc  7503  mullocpr  7508  distrlem4prl  7521  distrlem4pru  7522  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemopu  7540  cauappcvgprlemopl  7583  cauappcvgprlemopu  7585  cauappcvgprlemdisj  7588  cauappcvgprlem2  7597  cauappcvgprlemlim  7598  caucvgprlemnkj  7603  caucvgprlemopl  7606  caucvgprlemopu  7608  caucvgprlemdisj  7611  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem2  7617  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemlol  7635  caucvgprprlemexbt  7643  caucvgprprlem1  7646  suplocexprlemrl  7654  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  prsrlem1  7679  gt0srpr  7685  caucvgsrlemcl  7726  caucvgsrlembound  7731  caucvgsrlemgt1  7732  suplocsrlemb  7743  suplocsrlem  7745  suplocsr  7746  ltresr  7776  nnindnn  7830  axcaucvglemcl  7832  axcaucvglemval  7834  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  axpre-suploc  7839  sup3exmid  8848  nnind  8869  nn0supp  9162  nn0ge2m1nn  9170  zleloe  9234  zapne  9261  nn0lt2  9268  suprzclex  9285  zindd  9305  uzm1  9492  uzin  9494  infregelbex  9532  elnn1uz2  9541  nn01to3  9551  divfnzn  9555  qapne  9573  xrltnsym2  9726  xaddass  9801  xleadd1a  9805  xlt2add  9812  xlesubadd  9815  iooval2  9847  icoshftf1o  9923  fztri3or  9970  fzneuz  10032  4fvwrd4  10071  elfzo0  10113  exbtwnzlemex  10181  ioom  10192  fzfig  10361  uzennn  10367  uzsinds  10373  iseqovex  10387  seq3val  10389  seqvalcd  10390  seqf  10392  seqovcd  10394  monoord2  10408  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  seq3f1olemqsum  10431  seq3f1o  10435  seq3distr  10444  expp1  10458  expcl2lemap  10463  expclzap  10476  expap0i  10483  nn0ltexp2  10619  bcval5  10672  hashinfuni  10686  hashennnuni  10688  hashnncl  10705  resunimafz0  10740  zfz1isolemiso  10748  zfz1isolem1  10749  zfz1iso  10750  seq3shft  10776  cvg1nlemcau  10922  rexanuz  10926  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemsqa  10962  resqrexlemex  10963  rersqreu  10966  caubnd2  11055  maxleast  11151  fimaxre2  11164  minmax  11167  xrmaxiflemcl  11182  xrmaxiflemab  11184  xrmaxiflemlub  11185  xrmaxadd  11198  xrminmax  11202  xrbdtri  11213  climreu  11234  reccn2ap  11250  iserex  11276  climcvg1nlem  11286  serf0  11289  fz1f1o  11312  summodclem3  11317  zsumdc  11321  fsum3  11324  isumz  11326  isumss  11328  isumss2  11330  fsumsersdc  11332  fsum3ser  11334  fsumsplit  11344  isumclim2  11359  isumclim3  11360  fsum2dlemstep  11371  fsumcnv  11374  fisumcom2  11375  bcxmas  11426  isumle  11432  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratz  11469  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  zproddc  11516  prod1dc  11523  fprodsplitdc  11533  fprodsplit  11534  fprodunsn  11541  fprodcl2lem  11542  fprodcllemf  11550  fprod2dlemstep  11559  fprodcnv  11562  fprodcom2fi  11563  fprodle  11577  ef0lem  11597  mod2eq1n2dvds  11812  ndvdssub  11863  infssuzex  11878  infssuzcldc  11880  suprzubdc  11881  nninfdcex  11882  zsupssdc  11883  gcdsupex  11886  gcdsupcl  11887  bezoutlemnewy  11925  bezoutlemmain  11927  bezoutlembi  11934  bezoutlemeu  11936  bezoutlemle  11937  uzwodc  11966  nnwofdc  11967  nnwosdc  11968  nn0seqcvgd  11969  eucalgf  11983  eucalginv  11984  lcmval  11991  prmind2  12048  dfphi2  12148  phiprmpw  12150  phimullem  12153  eulerthlem1  12155  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  eulerth  12161  phisum  12168  odzcllem  12170  odzdvds  12173  pythagtriplem19  12210  pclemub  12215  pcprecl  12217  pceu  12223  pcqmul  12231  pcqcl  12234  pcxnn0cl  12238  pcge0  12240  pcdvdsb  12247  pceq0  12249  pcneg  12252  pcdvdstr  12254  pcgcd1  12255  pc2dvds  12257  pcz  12259  pcprmpw2  12260  pcaddlem  12266  pcadd  12267  pcmptcl  12268  pcmpt  12269  pcmptdvds  12271  fldivp1  12274  qexpz  12278  pockthlem  12282  pockthg  12283  prmunb  12288  1arith  12293  ennnfonelemom  12337  ennnfoneleminc  12340  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemdm  12349  ennnfonelemr  12352  ennnfonelemim  12353  exmidunben  12355  ctinfom  12357  inffinp1  12358  ctinf  12359  enctlem  12361  ctiunctlemu1st  12363  ctiunctlemu2nd  12364  ctiunctlemudc  12366  ctiunct  12369  ctiunctal  12370  unct  12371  ssomct  12374  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  structcnvcnv  12406  setscom  12430  restid2  12560  topontopon  12618  eltg3i  12656  epttop  12690  difopn  12708  uncld  12713  0nnei  12753  resttopon  12771  restabs  12775  restopnb  12781  lmcvg  12817  cnptopco  12822  cnss1  12826  cnss2  12827  cncnpi  12828  cncnp2m  12831  cnrest  12835  cnrest2  12836  cnrest2r  12837  cnptoprest  12839  cnptoprest2  12840  lmss  12846  lmff  12849  lmtopcnp  12850  lmcn  12851  txbasval  12867  upxp  12872  txcnmpt  12873  txdis1cn  12878  txlm  12879  lmcn2  12880  cnmpt11  12883  cnmpt11f  12884  cnmpt1t  12885  cnmpt12  12887  cnmpt21  12891  cnmpt21f  12892  cnmpt2t  12893  cnmpt22  12894  cnmpt22f  12895  cnmptcom  12898  hmeocnv  12907  hmeof1o  12909  hmeores  12915  txhmeo  12919  txswaphmeo  12921  isxmet2d  12948  blfvalps  12985  xblss2ps  13004  xblss2  13005  blfps  13009  blf  13010  unirnblps  13022  unirnbl  13023  isxms2  13052  bdxmet  13101  bdmet  13102  xmetxp  13107  xmettx  13110  blssioo  13145  tgioo  13146  mulcncflem  13190  dedekindeulemuub  13195  dedekindeulemub  13196  dedekindeulemloc  13197  dedekindeulemlu  13199  suplociccreex  13202  suplociccex  13203  dedekindicclemuub  13204  dedekindicclemub  13205  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemuopn  13216  limcrcl  13227  limcmpted  13232  limccnp2lem  13245  limccnp2cntop  13246  limccoap  13247  dvrecap  13277  cosordlem  13370  logbgcd1irraplemexp  13486  logbgcd1irrap  13488  lgsneg1  13526  lgsdilem  13528  lgsdir2  13534  lgsdirprm  13535  lgsdir  13536  lgsne0  13539  lgsabs1  13540  lgsdirnn0  13548  lgsdinn0  13549  2sqlem5  13555  2sqlem7  13557  2sqlem8a  13558  2sqlem8  13559  2sqlem9  13560  bj-stand  13589  bj-charfundcALT  13651  bj-charfunbi  13653  bj-bdfindis  13789  bj-peano4  13797  strcollnfALT  13828  pwtrufal  13837  pwf1oexmid  13839  exmid1stab  13840  subctctexmid  13841  pw1nct  13843  nnsf  13845  nninfalllem1  13848  nninfall  13849  nninfsellemqall  13855  exmidsbthrlem  13861  sbthom  13865  cvgcmp2nlemabs  13871  trilpo  13882  iswomni0  13890  redcwlpo  13894  dceqnconst  13898  dcapnconst  13899  nconstwlpolem  13903  nconstwlpo  13904  neapmkvlem  13905  neapmkv  13906  taupi  13909  alsi1d  13917  alsi2d  13918  alsc1d  13919  alsc2d  13920