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	⊢ (𝜑 ↔ 𝜓)
sylbi.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbi	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
3		sylbi.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

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  7384  djuss  7410  eldju2ndl  7412  eldju2ndr  7413  ctssdclemr  7452  exmidlpo  7483  finnum  7528  ficardon  7534  exmidfodomrlemim  7553  acnrcl  7557  3nsssucpw1  7595  indpi  7709  subhalfnqq  7781  archnqq  7784  enq0sym  7799  nqnq0pi  7805  nqnq0  7808  mulnnnq0  7817  prml  7844  prmu  7845  prssnql  7846  prssnqu  7847  prcdnql  7851  prcunqu  7852  prltlu  7854  prnmaxl  7855  prnminu  7856  prloc  7858  prdisj  7859  addcanprg  7983  recexprlemopl  7992  recexprlemopu  7994  cauappcvgprlemladdfu  8021  caucvgprlemladdfu  8044  recexgt0sr  8140  renfdisj  8385  axsuploc  8398  negf1o  8709  recexre  8907  apsqgt0  8930  apreim  8932  aprcl  8975  recexaplem2  8981  rerecclap  9061  nn0ge0  9590  elnnnn0b  9609  xnn0xr  9637  xnn0nemnf  9643  xnn0nnn0pnf  9645  znegcl  9677  zeo  9753  nn0ind  9762  nn0ind-raph  9765  uzn0  9940  eluzaddi  9951  eluzsubi  9952  uznn0sub  9956  uz3m2nn  9975  uznnssnn  9979  uz2m1nn  10007  uz2mulcl  10010  indstr2  10011  qmulz  10025  qre  10027  qnegcl  10038  qreccl  10044  rphalflt  10086  nn0ledivnn  10170  xrltnr  10183  nltpnft  10218  ngtmnft  10221  xrrebnd  10223  xnegcl  10236  xnegneg  10237  xltnegi  10239  xrpnfdc  10246  xrmnfdc  10247  xnegid  10263  xaddid1  10266  xnn0lenn0nn0  10269  xnn0xadd0  10271  xposdif  10286  elioore  10316  elfzuz2  10435  uzsubsubfz  10454  fzdisj  10459  fzmmmeqm  10466  elfz0ubfz0  10534  elfz0fzfz0  10535  fz0fzelfz0  10536  fz0fzdiffz0  10539  elfzmlbp  10541  difelfzle  10543  difelfznle  10544  nn0disj  10547  2ffzeq  10550  fzo1fzo0n0  10597  elfzo0z  10598  elfzo0le  10599  fzonmapblen  10601  fzofzim  10602  elfzodifsumelfzo  10621  elfzonlteqm1  10630  fzonn0p1p1  10633  elfzom1p1elfzo  10634  ssfzo12bi  10645  ubmelm1fzo  10646  fzind2  10660  subfzo0  10663  infssuzcldc  10670  rebtwn2z  10691  fldiv4p1lem1div2  10742  fldiv4lem1div2  10744  flqeqceilz  10757  zmodidfzoimp  10793  modfzo0difsn  10834  nnsinds  10884  nn0sinds  10885  expcl2lemap  10990  qexpclz  10999  zzlesq  11148  facp1  11170  facnn2  11174  faclbnd3  11183  bcn1  11198  hashfz0  11268  hashfibc  11285  hashf1lem2  11288  wrdf  11312  swrdswrdlem  11478  swrdswrd  11479  swrdccatin1  11499  pfxccatin12lem2a  11501  pfxccatin12lem1  11502  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12lem3  11506  pfxccatin12  11507  pfxccat3  11508  swrdccat  11509  swrdccat3blem  11513  cvg1nlemres  11753  rexanuz  11756  fclim  12062  climmo  12066  iser3shft  12114  fsumsplitsn  12179  fsum2dlemstep  12203  fisumcom2  12207  arisum  12267  arisum2  12268  prodmodc  12347  fprodfac  12384  fprod2dlemstep  12391  fprodcom2fi  12395  fprodsplitsn  12402  eftlub  12459  ef01bndlem  12525  sin01gt0  12531  cos01gt0  12532  sin02gt0  12533  dvdsdivcl  12619  addmodlteqALT  12628  odd2np1  12642  oddge22np1  12650  m1expe  12668  nn0enne  12671  nn0o1gt2  12674  nno  12675  ndvdsadd  12700  dfgcd2  12793  mulgcd  12795  algfx  12832  prmind2  12900  prm2orodd  12906  prmgt1  12912  oddprmgt2  12914  dfphi2  13000  nnnn0modprm0  13036  prm23lt5  13044  pythagtriplem2  13047  pcz  13113  dvdsprmpweqnn  13117  oddprmdvds  13135  prmunb  13143  4sqlem4  13173  4sqlem19  13190  ballotfilem2  13230  ballotfilem7  13281  evenennn  13286  fngzsum  13710  gzsumvalx  13711  dfgrp3me  13907  mulgnn0gzsum  13933  rngdi  14241  rngdir  14242  dvdsrcl2  14408  unitinvcl  14432  unitinvinv  14433  unitlinv  14435  unitrinv  14436  opprdrng  14622  rmodislmodlem  14689  rmodislmod  14690  zrhval  14954  psrbagf  15056  distop  15188  ntrss  15222  ssntr  15225  lmrcl  15295  txuni2  15359  txcn  15378  hmeocnvb  15421  xmetunirn  15461  blssioo  15656  divcnap  15668  cdivcncfap  15707  dedekindeulemlub  15723  dedekindicclemlub  15732  dvexp2  15815  elply2  15838  plyco  15862  pilem3  15887  sincosq1sgn  15930  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  logfac  16001  birthdaylem1g  16093  fsumdvdsmul  16111  zabsle1  16130  lgsdir2lem4  16162  gausslemma2dlem0f  16185  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  gausslemma2dlem3  16194  gausslemma2dlem4  16195  2lgslem1a1  16217  2lgslem3  16232  2lgsoddprmlem3  16242  2lgsoddprm  16244  2sqlem2  16246  2sqlem10  16256  vtxvalprc  16308  iedgvalprc  16309  upgrex  16356  umgredg  16398  ausgrusgrben  16421  usgruspgrben  16439  usgrislfuspgrdom  16443  uhgr2edg  16459  uspgredg2v  16474  griedg0ssusgr  16504  subusgr  16528  wlkv  16579  wlk1walkdom  16612  trlsv  16637  trlf1  16641  clwwlk1loop  16652  clwwlkext2edg  16675  umgr2cwwkdifex  16678  clwwlknonex2lem2  16691  clwwlknonex2e  16693  eupthv  16699  eupth2lem3lem4fi  16726  konigsberglem5  16745  bj-pm2.18st  16790  bj-dcstab  16796  decidi  16835  sumdc2  16839  bj-charfunbi  16849  bdel  16883  bdssex  16940  bj-indind  16970  findset  16983  wexmiddc  17054  wexmiddifxy  17058  nninfall  17064  trirec0  17105  neap0mkv  17131  alsex  17151  ralsex  17152