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  1289  ecase23d  1332  exlimdh  1576  nexd  1593  alexnim  1628  excomim  1643  19.41  1666  equcomd  1687  nfexd  1741  sbh  1756  sbcof2  1790  sbidm  1831  sb6rf  1833  nfsbt  1956  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  eu2  2050  2euex  2093  eqcomd  2163  3eltr3g  2242  abbid  2274  neneqd  2348  eqnetrrid  2358  3netr3g  2361  necomd  2413  r19.21bi  2545  nrexdv  2550  rexlimd  2571  rabbidva  2700  elisset  2726  euind  2899  rmoan  2912  reuind  2917  2rmorex  2918  spsbc  2948  spesbc  3022  eldifad  3113  eldifbd  3114  3sstr3g  3170  sseqtrdi  3176  difindiss  3361  un00  3440  undifss  3474  ifcldcd  3540  disjpr2  3623  difprsn1  3695  diftpsn3  3697  difsnss  3702  sneqr  3723  preqr1  3731  preq12b  3733  oprcl  3765  intab  3836  riinm  3921  rintm  3941  disjiun  3960  sndisj  3961  3brtr3g  3997  trint  4077  iinexgm  4115  exmidexmid  4156  exmid01  4158  pwntru  4159  pwel  4177  exss  4186  0nelop  4207  euotd  4213  opelopabsb  4219  pwunim  4245  issod  4278  frind  4311  suctr  4380  orduniss  4384  onelini  4389  oneluni  4390  eusv2i  4413  rexxfrd  4421  rabxfrd  4427  reuhypd  4429  iunpw  4438  sucexg  4455  ordsucim  4457  ordtriexmidlem  4476  ontriexmidim  4479  ordtri2or2exmidlem  4483  onsucelsucexmidlem  4486  ordsucunielexmid  4488  orddif  4504  suc11g  4514  onintexmid  4530  reg3exmidlemwe  4536  tfisi  4544  peano1  4551  peano2  4552  finds2  4558  omsinds  4579  brrelex12  4621  brel  4635  ssrel  4671  ssrel2  4673  ssrelrel  4683  elrel  4685  xpsspw  4695  relop  4733  dmxpm  4803  opelresi  4874  ndmima  4960  poirr2  4975  xpmlem  5003  xpimasn  5031  iotass  5149  iotacl  5155  dffun5r  5179  funeu  5192  funeu2  5193  funfnd  5198  funopg  5201  funun  5211  funinsn  5216  funtp  5220  funcnvuni  5236  funcnvres2  5242  imadiflem  5246  imadif  5247  funimaexglem  5250  fneu2  5272  fnimaeq0  5288  fnmpt  5293  fun2  5340  f00  5358  f0bi  5359  foimacnv  5429  resdif  5433  f1ococnv1  5440  fv3  5488  relelfvdm  5497  nfvres  5498  dffn5im  5511  mptfvex  5550  fvmptdf  5552  fvmptdv2  5554  fndmdif  5569  dff4im  5610  fmpt  5614  fmptd  5618  fmptdf  5621  f1oresrab  5629  fcoconst  5635  fsn  5636  ftpg  5648  fsnunf  5664  resfunexg  5685  isores1  5759  riota2df  5794  acexmidlemcase  5813  brabvv  5861  funoprabg  5914  fnovim  5923  ovmpodf  5946  ovi3  5951  grprinvlem  6009  grprinvd  6010  grpridd  6011  elmpocl  6012  1stcof  6105  2ndcof  6106  fnmpo  6144  fmpoco  6157  fo2ndf  6168  f1o2ndf1  6169  disjxp1  6177  brtpos2  6192  reldmtpos  6194  dftpos3  6203  dftpos4  6204  tpostpos2  6206  tposf2  6209  tposf12  6210  tposfo  6212  tposf  6213  smores2  6235  tfrlem1  6249  tfrlem3-2d  6253  tfrlemisucaccv  6266  tfrlemibxssdm  6268  tfrlemibfn  6269  tfrlemi1  6273  tfrexlem  6275  tfr1onlemsucaccv  6282  tfr1onlembxssdm  6284  tfr1onlembfn  6285  tfr1onlemaccex  6289  tfrcllemsucaccv  6295  tfrcllembxssdm  6297  tfrcllembfn  6298  tfrcllemaccex  6302  tfrcldm  6304  rdgivallem  6322  rdgisucinc  6326  frecabex  6339  frecfnom  6342  frecfcllem  6345  frecsuclem  6347  omsuc  6412  nntri2  6434  nnsucuniel  6435  nnsseleq  6441  nnm00  6469  ecexr  6478  swoer  6501  elqsn0m  6541  iinerm  6545  erinxp  6547  ecinxp  6548  eroveu  6564  eroprf  6566  mapprc  6590  mapsn  6628  ixpprc  6657  ixp0  6669  resixp  6671  elixpsn  6673  dom2lem  6710  fundmen  6744  dom0  6776  xpf1o  6782  mapxpen  6786  xpmapenlem  6787  ssenen  6789  nneneq  6795  ssfilem  6813  dif1en  6817  dif1enen  6818  fin0  6823  fin0or  6824  diffitest  6825  diffisn  6831  ac6sfi  6836  fimax2gtrilemstep  6838  fimax2gtri  6839  finexdc  6840  exmidpweq  6847  pw1fin  6848  onunsnss  6854  unsnfidcel  6858  undifdcss  6860  undifdc  6861  fiintim  6866  fisseneq  6869  fidcenumlemr  6892  sbthlemi4  6897  sbthlemi5  6898  sbthlemi9  6902  fifo  6917  suplubti  6936  supelti  6938  infmoti  6964  infisoti  6968  djulclb  6989  updjud  7016  omp1eomlem  7028  0ct  7041  ctmlemr  7042  ctssdclemn0  7044  ctssdccl  7045  ctssdc  7047  enumct  7049  finomni  7066  fodjuomnilemdc  7070  fodjum  7072  fodjuomnilemres  7074  fodjumkvlemres  7085  omniwomnimkv  7093  exmidonfinlem  7111  en2eleq  7113  exmidfodomrlemeldju  7117  exmidfodomrlemreseldju  7118  exmidfodomrlemim  7119  acfun  7125  exmidaclem  7126  exmidontriimlem3  7141  exmidontriimlem4  7142  exmidontriim  7143  pw1on  7144  ccfunen  7167  cc1  7168  cc2lem  7169  cc2  7170  cc3  7171  elni2  7217  indpi  7245  distrnqg  7290  subhalfnqq  7317  enq0sym  7335  enq0ref  7336  enq0tr  7337  nqnq0pi  7341  nnnq0lem1  7349  distrnq0  7362  elinp  7377  elnp1st2nd  7379  prltlu  7390  prnmaxl  7391  prnminu  7392  prarloc  7406  nqprm  7445  appdivnq  7466  prmuloc  7469  mullocpr  7474  distrlem4prl  7487  distrlem4pru  7488  ltexprlemm  7503  ltexprlemopl  7504  ltexprlemopu  7506  cauappcvgprlemopl  7549  cauappcvgprlemopu  7551  cauappcvgprlemdisj  7554  cauappcvgprlem2  7563  cauappcvgprlemlim  7564  caucvgprlemnkj  7569  caucvgprlemopl  7572  caucvgprlemopu  7574  caucvgprlemdisj  7577  caucvgprlemcl  7579  caucvgprlemladdfu  7580  caucvgprlemladdrl  7581  caucvgprlem2  7583  caucvgprprlemcbv  7590  caucvgprprlemval  7591  caucvgprprlemlol  7601  caucvgprprlemexbt  7609  caucvgprprlem1  7612  suplocexprlemrl  7620  suplocexprlemmu  7621  suplocexprlemru  7622  suplocexprlemdisj  7623  suplocexprlemloc  7624  suplocexprlemub  7626  suplocexprlemlub  7627  prsrlem1  7645  gt0srpr  7651  caucvgsrlemcl  7692  caucvgsrlembound  7697  caucvgsrlemgt1  7698  suplocsrlemb  7709  suplocsrlem  7711  suplocsr  7712  ltresr  7742  nnindnn  7796  axcaucvglemcl  7798  axcaucvglemval  7800  axcaucvglemcau  7801  axcaucvglemres  7802  axpre-suploclemres  7804  axpre-suploc  7805  sup3exmid  8811  nnind  8832  nn0supp  9125  nn0ge2m1nn  9133  zleloe  9197  zapne  9221  nn0lt2  9228  suprzclex  9245  zindd  9265  uzm1  9452  uzin  9454  elnn1uz2  9500  nn01to3  9508  divfnzn  9512  qapne  9530  xrltnsym2  9683  xaddass  9755  xleadd1a  9759  xlt2add  9766  xlesubadd  9769  iooval2  9801  icoshftf1o  9877  fztri3or  9923  fzneuz  9985  4fvwrd4  10021  elfzo0  10063  exbtwnzlemex  10131  ioom  10142  fzfig  10311  uzennn  10317  uzsinds  10323  iseqovex  10337  seq3val  10339  seqvalcd  10340  seqf  10342  seqovcd  10344  monoord2  10358  iseqf1olemjpcl  10376  iseqf1olemqpcl  10377  seq3f1olemqsum  10381  seq3f1o  10385  seq3distr  10394  expp1  10408  expcl2lemap  10413  expclzap  10426  expap0i  10433  bcval5  10619  hashinfuni  10633  hashennnuni  10635  hashnncl  10652  resunimafz0  10684  zfz1isolemiso  10692  zfz1isolem1  10693  zfz1iso  10694  seq3shft  10720  cvg1nlemcau  10866  rexanuz  10870  resqrexlemoverl  10903  resqrexlemglsq  10904  resqrexlemsqa  10906  resqrexlemex  10907  rersqreu  10910  caubnd2  10999  maxleast  11095  fimaxre2  11108  minmax  11111  xrmaxiflemcl  11124  xrmaxiflemab  11126  xrmaxiflemlub  11127  xrmaxadd  11140  xrminmax  11144  xrbdtri  11155  climreu  11176  reccn2ap  11192  iserex  11218  climcvg1nlem  11228  serf0  11231  fz1f1o  11254  summodclem3  11259  zsumdc  11263  fsum3  11266  isumz  11268  isumss  11270  isumss2  11272  fsumsersdc  11274  fsum3ser  11276  fsumsplit  11286  isumclim2  11301  isumclim3  11302  fsum2dlemstep  11313  fsumcnv  11316  fisumcom2  11317  bcxmas  11368  isumle  11374  cvgratnnlemnexp  11403  cvgratnnlemmn  11404  cvgratz  11411  mertenslemub  11413  mertenslemi1  11414  mertenslem2  11415  mertensabs  11416  zproddc  11458  prod1dc  11465  fprodsplitdc  11475  fprodsplit  11476  fprodunsn  11483  fprodcl2lem  11484  fprodcllemf  11492  fprod2dlemstep  11501  fprodcnv  11504  fprodcom2fi  11505  fprodle  11519  ef0lem  11539  mod2eq1n2dvds  11751  ndvdssub  11802  infssuzex  11817  infssuzcldc  11819  gcdsupex  11821  gcdsupcl  11822  bezoutlemnewy  11860  bezoutlemmain  11862  bezoutlembi  11869  bezoutlemeu  11871  bezoutlemle  11872  nn0seqcvgd  11898  eucalgf  11912  eucalginv  11913  lcmval  11920  prmind2  11977  dfphi2  12072  phiprmpw  12074  phimullem  12077  eulerthlem1  12079  eulerthlemrprm  12081  eulerthlema  12082  eulerthlemh  12083  eulerthlemth  12084  eulerth  12085  phisum  12092  ennnfonelemom  12109  ennnfoneleminc  12112  ennnfonelemhf1o  12114  ennnfonelemex  12115  ennnfonelemhom  12116  ennnfonelemdm  12121  ennnfonelemr  12124  ennnfonelemim  12125  exmidunben  12127  ctinfom  12129  inffinp1  12130  ctinf  12131  enctlem  12133  ctiunctlemu1st  12135  ctiunctlemu2nd  12136  ctiunctlemudc  12138  ctiunct  12141  ctiunctal  12142  unct  12143  structcnvcnv  12166  setscom  12190  restid2  12320  topontopon  12378  eltg3i  12416  epttop  12450  difopn  12468  uncld  12473  0nnei  12513  resttopon  12531  restabs  12535  restopnb  12541  lmcvg  12577  cnptopco  12582  cnss1  12586  cnss2  12587  cncnpi  12588  cncnp2m  12591  cnrest  12595  cnrest2  12596  cnrest2r  12597  cnptoprest  12599  cnptoprest2  12600  lmss  12606  lmff  12609  lmtopcnp  12610  lmcn  12611  txbasval  12627  upxp  12632  txcnmpt  12633  txdis1cn  12638  txlm  12639  lmcn2  12640  cnmpt11  12643  cnmpt11f  12644  cnmpt1t  12645  cnmpt12  12647  cnmpt21  12651  cnmpt21f  12652  cnmpt2t  12653  cnmpt22  12654  cnmpt22f  12655  cnmptcom  12658  hmeocnv  12667  hmeof1o  12669  hmeores  12675  txhmeo  12679  txswaphmeo  12681  isxmet2d  12708  blfvalps  12745  xblss2ps  12764  xblss2  12765  blfps  12769  blf  12770  unirnblps  12782  unirnbl  12783  isxms2  12812  bdxmet  12861  bdmet  12862  xmetxp  12867  xmettx  12870  blssioo  12905  tgioo  12906  mulcncflem  12950  dedekindeulemuub  12955  dedekindeulemub  12956  dedekindeulemloc  12957  dedekindeulemlu  12959  suplociccreex  12962  suplociccex  12963  dedekindicclemuub  12964  dedekindicclemub  12965  dedekindicclemloc  12966  dedekindicclemlu  12968  dedekindicc  12971  ivthinclemlopn  12974  ivthinclemuopn  12976  limcrcl  12987  limcmpted  12992  limccnp2lem  13005  limccnp2cntop  13006  limccoap  13007  dvrecap  13037  cosordlem  13130  logbgcd1irraplemexp  13245  logbgcd1irrap  13247  bj-stand  13280  bj-charfundcALT  13343  bj-charfunbi  13345  bj-bdfindis  13481  bj-peano4  13489  strcollnfALT  13520  pwtrufal  13529  pwf1oexmid  13531  exmid1stab  13532  subctctexmid  13533  pw1nct  13535  nnsf  13538  nninfalllem1  13542  nninfall  13543  nninfsellemqall  13549  exmidsbthrlem  13555  sbthom  13559  cvgcmp2nlemabs  13565  trilpo  13576  iswomni0  13584  redcwlpo  13588  dceqnconst  13592  dcapnconst  13593  nconstwlpolem  13597  nconstwlpo  13598  neapmkvlem  13599  neapmkv  13600  taupi  13603  alsi1d  13611  alsi2d  13612  alsc1d  13613  alsc2d  13614