Theorem sylbi 121

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylbi.1	|- ( ph <-> ps )
sylbi.2	|- ( ps -> ch )

Assertion

Ref	Expression
sylbi	|- ( ph -> ch )

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 120	. 2 |- ( ph -> ps )
3		sylbi.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  391  mpan10  478  an12s  571  an32s  574  an4s  596  sylnbi  689  dcim  853  notnotrdc  855  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.25dc  905  pm2.85dc  917  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  peircedc  926  pm5.54dc  930  dcand  945  dcor  948  pm5.62dc  958  pm5.63dc  959  pm4.83dc  964  ifp2  993  ifpor  1000  1fpid3  1007  3simpb  1026  3simpc  1027  3imp  1224  3com12  1238  3com13  1239  syl3anb  1321  xoranor  1426  xorbin  1433  xordc1  1442  biassdc  1444  nfr  1571  nfand  1621  19.21t  1635  19.30dc  1680  exintrbi  1686  19.9t  1695  nfnt  1708  equveli  1812  exdistrfor  1853  sbcof2  1863  sbidm  1904  sbi1v  1946  sbalyz  2059  sbal1yz  2061  nfsb4t  2074  euex  2116  eumo0  2117  mor  2129  exmodc  2137  mo3h  2140  mopick  2165  moexexdc  2171  euexex  2172  2euex  2174  exists2  2184  eqcoms  2241  eleq2s  2333  nfcr  2384  necon3ai  2469  rexnalim  2539  dfrex2dc  2541  rexex  2596  rsp  2597  ralim  2609  rexim  2644  r19.32r  2697  r19.44av  2710  r19.45av  2711  gencl  2854  gencbvex  2869  gencbval  2871  vtoclgf  2881  vtoclg1f  2882  pm13.183  2964  elrabi  2979  eueq2dc  2999  eueq3dc  3000  mob2  3006  euxfr2dc  3011  reu3  3016  rmoim  3027  2rmorex  3032  sbcex  3060  sbcbi2  3102  ra5  3141  sseq1  3271  difdif  3354  dfss4st  3464  difindiss  3485  undif3ss  3492  dfrab3ss  3511  abvor0dc  3545  reldisj  3576  disjel  3579  inssdif0imOLD  3593  uneqdifeqim  3613  r19.2m  3614  r19.2mOLD  3615  r19.3rm  3616  r19.9rmv  3619  rexm  3627  ralm  3631  raaanlem  3632  ifnefalse  3651  ifnotdc  3679  ifandc  3681  ifmdc  3683  nelpri  3733  nelprd  3735  prprc1  3821  difprsn2  3855  diftpsn3  3856  snsssn  3886  preqr2  3894  preq12b  3895  opthpr  3897  prneimg  3899  oprcl  3928  pwprss  3931  intmin4  3998  uniintabim  4007  dfiin2g  4045  iinss2  4065  iundif2ss  4078  disjnim  4120  disjnims  4121  invdisj  4123  disjiun  4125  brne0  4180  brm  4181  trel  4236  trss  4238  ssex  4270  bnd2  4310  abssexg  4319  exmidexmid  4333  rext  4355  unipw  4357  euabex  4365  mss  4366  exss  4367  copsexg  4384  opelopabsb  4402  pwssunim  4429  epelg  4435  sowlin  4465  sotritric  4469  elsuci  4548  sucprc  4557  reusv3  4606  ordon  4633  onsucmin  4654  onsucelsucr  4655  unon  4658  onsucelsucexmid  4677  setind  4686  setind2  4687  sucprcreg  4696  en2lp  4701  eunex  4708  ordsoexmid  4709  ordpwsucss  4714  tfi  4729  peano1  4741  peano2  4742  find  4746  0nelelxp  4803  opelxp  4804  elvvuni  4839  optocl  4851  ralxpf  4926  rexxpf  4927  relop  4930  breldm  4985  reldmm  5000  dmxpm  5002  elreldm  5008  dmrnssfld  5045  dmcosseq  5054  resabs1  5092  resima2  5097  issref  5170  asymref  5173  xpidtr  5178  trin2  5179  poirr2  5180  xpmlem  5208  dmxpss  5218  xp11m  5226  cnveqb  5243  dfco2a  5288  cores2  5300  coi2  5304  relcnvtr  5307  relresfld  5317  relcnvexb  5327  cnviinm  5329  iotauni  5350  iota1  5352  iota4  5357  iotam  5369  dffun8  5405  fununfun  5424  funcnvsn  5426  imadif  5461  imainlem  5462  fcoi1  5572  fcoi2  5573  f0rn0  5587  f1ocnv  5652  f1ocnvb  5653  fun11iun  5660  ffoss  5672  f1o00  5676  fo00  5677  relelfvdm  5727  nfvres  5732  nfunsn  5733  ssimaex  5764  fvmptss2  5780  fvmptssdm  5790  unpreima  5833  respreima  5836  elrnrexdm  5847  elrnrexdmb  5848  rexrnmpt  5851  dffo4  5856  rnmptss  5869  funiun  5890  funopdmsn  5895  fvpr1  5919  fvpr2  5920  elunirn  5972  f1veqaeq  5975  isores1  6020  iotaexel  6043  riotauni  6045  riotacl2  6053  riota1  6058  riota1a  6059  snriota  6070  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  oprabid  6117  0neqopab  6133  brabvv  6134  1stval2  6389  2ndval2  6390  xp1st  6399  xp2nd  6400  unielxp  6408  releldm2  6419  cnvf1o  6461  fo2ndf  6463  poxp  6468  reldmtpos  6524  dftpos4  6534  tpostpos  6535  tpostpos2  6536  iunon  6555  smoel  6571  tfrlem4  6584  tfrlem7  6588  tfrlem8  6589  tfrlem9  6590  nnaord  6782  ecexr  6812  swoord1  6836  swoord2  6837  0er  6841  mapprc  6926  mapfoss  6947  fsetdmprc0  6950  mapsnconst  6976  ixpf  7002  mptelixpg  7016  idssen  7063  ener  7066  en0  7082  en1  7086  en1bg  7087  2dom  7093  modom  7108  enm  7118  xpsnen  7119  ssenen  7152  snnen2og  7160  php5dom  7164  phpm  7167  findcard  7192  findcard2  7193  findcard2s  7194  unfiexmid  7225  fiintim  7238  fidcenumlemim  7269  sbthlem1  7274  fiss  7311  djuexb  7385  djuss  7411  eldju2ndl  7413  eldju2ndr  7414  ctssdclemr  7453  exmidlpo  7484  finnum  7529  ficardon  7535  exmidfodomrlemim  7554  acnrcl  7558  3nsssucpw1  7596  indpi  7710  subhalfnqq  7782  archnqq  7785  enq0sym  7800  nqnq0pi  7806  nqnq0  7809  mulnnnq0  7818  prml  7845  prmu  7846  prssnql  7847  prssnqu  7848  prcdnql  7852  prcunqu  7853  prltlu  7855  prnmaxl  7856  prnminu  7857  prloc  7859  prdisj  7860  addcanprg  7984  recexprlemopl  7993  recexprlemopu  7995  cauappcvgprlemladdfu  8022  caucvgprlemladdfu  8045  recexgt0sr  8141  renfdisj  8386  axsuploc  8399  negf1o  8711  recexre  8909  apsqgt0  8932  apreim  8934  aprcl  8977  recexaplem2  8983  rerecclap  9063  nn0ge0  9593  elnnnn0b  9612  xnn0xr  9640  xnn0nemnf  9646  xnn0nnn0pnf  9648  znegcl  9680  zeo  9756  nn0ind  9765  nn0ind-raph  9768  uzn0  9948  eluzaddi  9959  eluzsubi  9960  uznn0sub  9964  uz3m2nn  9983  uznnssnn  9987  uz2m1nn  10015  uz2mulcl  10018  indstr2  10019  qmulz  10033  qre  10035  qnegcl  10046  qreccl  10052  rphalflt  10095  nn0ledivnn  10179  xrltnr  10192  nltpnft  10227  ngtmnft  10230  xrrebnd  10232  xnegcl  10245  xnegneg  10246  xltnegi  10248  xrpnfdc  10255  xrmnfdc  10256  xnegid  10272  xaddid1  10275  xnn0lenn0nn0  10278  xnn0xadd0  10280  xposdif  10295  elioore  10325  elfzuz2  10444  uzsubsubfz  10463  fzdisj  10468  fzmmmeqm  10475  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  difelfznle  10553  nn0disj  10556  2ffzeq  10559  fzo1fzo0n0  10606  elfzo0z  10607  elfzo0le  10608  fzonmapblen  10610  fzofzim  10611  elfzodifsumelfzo  10630  elfzonlteqm1  10639  fzonn0p1p1  10642  elfzom1p1elfzo  10643  ssfzo12bi  10654  ubmelm1fzo  10655  fzind2  10669  subfzo0  10672  infssuzcldc  10679  rebtwn2z  10700  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  flqeqceilz  10770  zmodidfzoimp  10806  modfzo0difsn  10847  nnsinds  10897  nn0sinds  10898  expcl2lemap  11003  qexpclz  11012  zzlesq  11161  facp1  11184  facnn2  11188  faclbnd3  11197  bcn1  11212  hashfz0  11282  hashfibc  11299  hashf1lem2  11302  wrdf  11326  swrdswrdlem  11492  swrdswrd  11493  swrdccatin1  11513  pfxccatin12lem2a  11515  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  swrdccat3blem  11527  cvg1nlemres  11767  rexanuz  11770  fclim  12079  climmo  12083  iser3shft  12131  fsumsplitsn  12196  fsum2dlemstep  12220  fisumcom2  12224  arisum  12284  arisum2  12285  prodmodc  12364  fprodfac  12401  fprod2dlemstep  12408  fprodcom2fi  12412  fprodsplitsn  12419  eftlub  12476  ef01bndlem  12542  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  dvdsdivcl  12636  addmodlteqALT  12645  odd2np1  12659  oddge22np1  12667  m1expe  12685  nn0enne  12688  nn0o1gt2  12691  nno  12692  ndvdsadd  12717  dfgcd2  12810  mulgcd  12812  algfx  12849  prmind2  12917  prm2orodd  12923  prmgt1  12930  oddprmgt2  12932  dfphi2  13021  nnnn0modprm0  13057  prm23lt5  13065  pythagtriplem2  13068  pcz  13134  dvdsprmpweqnn  13138  oddprmdvds  13156  prmunb  13164  4sqlem4  13194  4sqlem19  13211  ballotfilem2  13280  ballotfilem7  13331  evenennn  13336  fngzsum  13761  gzsumvalx  13762  dfgrp3me  13958  mulgnn0gzsum  13984  rngdi  14323  rngdir  14324  dvdsrcl2  14490  unitinvcl  14514  unitinvinv  14515  unitlinv  14517  unitrinv  14518  opprdrng  14704  rmodislmodlem  14771  rmodislmod  14772  zrhval  15036  psrbagf  15138  distop  15277  ntrss  15311  ssntr  15314  lmrcl  15384  txuni2  15448  txcn  15467  hmeocnvb  15510  xmetunirn  15550  blssioo  15745  divcnap  15757  cdivcncfap  15796  dedekindeulemlub  15812  dedekindicclemlub  15821  dvexp2  15904  elply2  15927  plyco  15951  pilem3  15976  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  logfac  16090  birthdaylem1g  16186  fsumdvdsmul  16246  bpos1  16271  zabsle1  16284  lgsdir2lem4  16316  gausslemma2dlem0f  16339  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem3  16348  gausslemma2dlem4  16349  2lgslem1a1  16371  2lgslem3  16386  2lgsoddprmlem3  16396  2lgsoddprm  16398  2sqlem2  16400  2sqlem10  16410  vtxvalprc  16462  iedgvalprc  16463  upgrex  16510  umgredg  16552  ausgrusgrben  16575  usgruspgrben  16593  usgrislfuspgrdom  16597  uhgr2edg  16613  uspgredg2v  16628  griedg0ssusgr  16658  subusgr  16682  wlkv  16733  wlk1walkdom  16766  trlsv  16791  trlf1  16795  clwwlk1loop  16806  clwwlkext2edg  16829  umgr2cwwkdifex  16832  clwwlknonex2lem2  16845  clwwlknonex2e  16847  eupthv  16853  eupth2lem3lem4fi  16880  konigsberglem5  16899  bj-pm2.18st  16944  bj-dcstab  16950  decidi  16989  sumdc2  16993  bj-charfunbi  17003  bdel  17037  bdssex  17094  bj-indind  17124  findset  17137  wexmiddc  17208  wexmiddifxy  17212  nninfall  17218  trirec0  17260  neap0mkv  17286  alsex  17306  ralsex  17307