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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  387  mpan10  474  an12s  565  an32s  568  an4s  588  sylnbi  678  dcim  841  notnotrdc  843  condcOLD  854  pm2.61ddc  861  pm5.18dc  883  pm2.25dc  893  pm2.85dc  905  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  peircedc  914  pm5.54dc  918  dcor  935  pm5.62dc  945  pm5.63dc  946  pm4.83dc  951  3simpb  995  3simpc  996  3imp  1193  3com12  1207  3com13  1208  syl3anb  1281  xoranor  1377  xorbin  1384  xordc1  1393  biassdc  1395  nfr  1518  nfand  1568  19.21t  1582  19.30dc  1627  exintrbi  1633  19.9t  1642  nfnt  1656  equveli  1759  exdistrfor  1800  sbcof2  1810  sbidm  1851  sbi1v  1891  sbalyz  1999  sbal1yz  2001  nfsb4t  2014  euex  2056  eumo0  2057  mor  2068  exmodc  2076  mo3h  2079  mopick  2104  moexexdc  2110  euexex  2111  2euex  2113  exists2  2123  eqcoms  2180  eleq2s  2272  nfcr  2311  necon3ai  2396  rexnalim  2466  dfrex2dc  2468  rexex  2523  rsp  2524  ralim  2536  rexim  2571  r19.32r  2623  r19.44av  2636  r19.45av  2637  gencl  2771  gencbvex  2785  gencbval  2787  vtoclgf  2797  vtoclg1f  2798  pm13.183  2877  elrabi  2892  eueq2dc  2912  eueq3dc  2913  mob2  2919  euxfr2dc  2924  reu3  2929  rmoim  2940  2rmorex  2945  sbcex  2973  sbcbi2  3015  ra5  3053  sseq1  3180  difdif  3262  dfss4st  3370  difindiss  3391  undif3ss  3398  dfrab3ss  3415  abvor0dc  3448  reldisj  3476  disjel  3479  inssdif0im  3492  uneqdifeqim  3510  r19.2m  3511  r19.2mOLD  3512  r19.3rm  3513  r19.9rmv  3516  rexm  3524  ralm  3529  raaanlem  3530  ifnefalse  3547  ifnotdc  3573  ifandc  3574  ifmdc  3576  nelpri  3618  nelprd  3620  prprc1  3702  difprsn2  3734  diftpsn3  3735  snsssn  3763  preqr2  3771  preq12b  3772  opthpr  3774  prneimg  3776  oprcl  3804  pwprss  3807  intmin4  3874  uniintabim  3883  dfiin2g  3921  iinss2  3941  iundif2ss  3954  disjnim  3996  disjnims  3997  invdisj  3999  disjiun  4000  brne0  4054  brm  4055  trel  4110  trss  4112  ssex  4142  bnd2  4175  abssexg  4184  exmidexmid  4198  rext  4217  unipw  4219  euabex  4227  mss  4228  exss  4229  copsexg  4246  opelopabsb  4262  pwssunim  4286  epelg  4292  sowlin  4322  sotritric  4326  elsuci  4405  sucprc  4414  reusv3  4462  ordon  4487  onsucmin  4508  onsucelsucr  4509  unon  4512  onsucelsucexmid  4531  setind  4540  setind2  4541  sucprcreg  4550  en2lp  4555  eunex  4562  ordsoexmid  4563  ordpwsucss  4568  tfi  4583  peano1  4595  peano2  4596  find  4600  0nelelxp  4657  opelxp  4658  elvvuni  4692  optocl  4704  ralxpf  4775  rexxpf  4776  relop  4779  breldm  4833  dmxpm  4849  elreldm  4855  dmrnssfld  4892  dmcosseq  4900  resabs1  4938  resima2  4943  issref  5013  asymref  5016  xpidtr  5021  trin2  5022  poirr2  5023  xpmlem  5051  dmxpss  5061  xp11m  5069  cnveqb  5086  dfco2a  5131  cores2  5143  coi2  5147  relcnvtr  5150  relresfld  5160  relcnvexb  5170  cnviinm  5172  iotauni  5192  iota1  5194  iota4  5198  iotam  5210  dffun8  5246  funcnvsn  5263  imadif  5298  imainlem  5299  fcoi1  5398  fcoi2  5399  f0rn0  5412  f1ocnv  5476  f1ocnvb  5477  fun11iun  5484  ffoss  5495  f1o00  5498  fo00  5499  relelfvdm  5549  nfvres  5550  nfunsn  5551  ssimaex  5579  fvmptss2  5593  fvmptssdm  5602  unpreima  5643  respreima  5646  elrnrexdm  5657  elrnrexdmb  5658  rexrnmpt  5661  dffo4  5666  rnmptss  5679  fvpr1  5722  fvpr2  5723  elunirn  5769  f1veqaeq  5772  isores1  5817  riotauni  5839  riotacl2  5846  riota1  5851  riota1a  5852  snriota  5862  eusvobj2  5863  acexmidlema  5868  acexmidlemb  5869  acexmidlem2  5874  oprabid  5909  0neqopab  5922  brabvv  5923  1stval2  6158  2ndval2  6159  xp1st  6168  xp2nd  6169  unielxp  6177  releldm2  6188  cnvf1o  6228  fo2ndf  6230  poxp  6235  reldmtpos  6256  dftpos4  6266  tpostpos  6267  tpostpos2  6268  iunon  6287  smoel  6303  tfrlem4  6316  tfrlem7  6320  tfrlem8  6321  tfrlem9  6322  nnaord  6512  ecexr  6542  swoord1  6566  swoord2  6567  0er  6571  mapprc  6654  mapsnconst  6696  ixpf  6722  mptelixpg  6736  idssen  6779  ener  6781  en0  6797  en1  6801  en1bg  6802  2dom  6807  enm  6822  xpsnen  6823  ssenen  6853  snnen2og  6861  php5dom  6865  phpm  6867  findcard  6890  findcard2  6891  findcard2s  6892  unfiexmid  6919  fiintim  6930  fidcenumlemim  6953  sbthlem1  6958  fiss  6978  djuexb  7045  djuss  7071  eldju2ndl  7073  eldju2ndr  7074  ctssdclemr  7113  exmidlpo  7143  finnum  7184  exmidfodomrlemim  7202  3nsssucpw1  7237  indpi  7343  subhalfnqq  7415  archnqq  7418  enq0sym  7433  nqnq0pi  7439  nqnq0  7442  mulnnnq0  7451  prml  7478  prmu  7479  prssnql  7480  prssnqu  7481  prcdnql  7485  prcunqu  7486  prltlu  7488  prnmaxl  7489  prnminu  7490  prloc  7492  prdisj  7493  addcanprg  7617  recexprlemopl  7626  recexprlemopu  7628  cauappcvgprlemladdfu  7655  caucvgprlemladdfu  7678  recexgt0sr  7774  renfdisj  8019  axsuploc  8032  negf1o  8341  recexre  8537  apsqgt0  8560  apreim  8562  aprcl  8605  recexaplem2  8611  rerecclap  8689  nn0ge0  9203  elnnnn0b  9222  xnn0xr  9246  xnn0nemnf  9252  xnn0nnn0pnf  9254  znegcl  9286  zeo  9360  nn0ind  9369  nn0ind-raph  9372  uzn0  9545  eluzaddi  9556  eluzsubi  9557  uznn0sub  9561  uz3m2nn  9575  uznnssnn  9579  uz2m1nn  9607  uz2mulcl  9610  indstr2  9611  qmulz  9625  qre  9627  qnegcl  9638  qreccl  9644  rphalflt  9685  nn0ledivnn  9769  xrltnr  9781  nltpnft  9816  ngtmnft  9819  xrrebnd  9821  xnegcl  9834  xnegneg  9835  xltnegi  9837  xrpnfdc  9844  xrmnfdc  9845  xnegid  9861  xaddid1  9864  xnn0lenn0nn0  9867  xnn0xadd0  9869  xposdif  9884  elioore  9914  elfzuz2  10031  uzsubsubfz  10049  fzdisj  10054  fzmmmeqm  10060  elfz0ubfz0  10127  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  elfzmlbp  10134  difelfzle  10136  difelfznle  10137  nn0disj  10140  2ffzeq  10143  fzo1fzo0n0  10185  elfzo0z  10186  elfzo0le  10187  fzonmapblen  10189  fzofzim  10190  elfzodifsumelfzo  10203  elfzonlteqm1  10212  fzonn0p1p1  10215  elfzom1p1elfzo  10216  ssfzo12bi  10227  ubmelm1fzo  10228  fzind2  10241  subfzo0  10244  rebtwn2z  10257  fldiv4p1lem1div2  10307  flqeqceilz  10320  zmodidfzoimp  10356  modfzo0difsn  10397  nnsinds  10445  nn0sinds  10446  expcl2lemap  10534  qexpclz  10543  facp1  10712  facnn2  10716  faclbnd3  10725  bcn1  10740  hashfz0  10807  cvg1nlemres  10996  rexanuz  10999  fclim  11304  climmo  11308  iser3shft  11356  fsumsplitsn  11420  fsum2dlemstep  11444  fisumcom2  11448  arisum  11508  arisum2  11509  prodmodc  11588  fprodfac  11625  fprod2dlemstep  11632  fprodcom2fi  11636  fprodsplitsn  11643  eftlub  11700  ef01bndlem  11766  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  dvdsdivcl  11858  addmodlteqALT  11867  odd2np1  11880  oddge22np1  11888  m1expe  11906  nn0enne  11909  nn0o1gt2  11912  nno  11913  ndvdsadd  11938  infssuzcldc  11954  dfgcd2  12017  mulgcd  12019  algfx  12054  prmind2  12122  prm2orodd  12128  prmgt1  12134  oddprmgt2  12136  dfphi2  12222  nnnn0modprm0  12257  prm23lt5  12265  pythagtriplem2  12268  pcz  12333  dvdsprmpweqnn  12337  oddprmdvds  12354  prmunb  12362  4sqlem4  12392  evenennn  12396  dfgrp3me  12975  dvdsrcl2  13273  unitinvcl  13297  unitinvinv  13298  unitlinv  13300  unitrinv  13301  rmodislmodlem  13445  rmodislmod  13446  distop  13624  ntrss  13658  ssntr  13661  lmrcl  13730  lmreltop  13732  txuni2  13795  txcn  13814  hmeocnvb  13857  xmetunirn  13897  blssioo  14084  divcnap  14094  cdivcncfap  14126  dedekindeulemlub  14137  dedekindicclemlub  14146  dvexp2  14215  pilem3  14243  sincosq1sgn  14286  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  sinq12gt0  14290  zabsle1  14439  lgsdir2lem4  14471  2lgsoddprmlem3  14498  2sqlem2  14501  2sqlem10  14511  bj-pm2.18st  14541  bj-dcstab  14547  decidi  14586  sumdc2  14590  bj-charfunbi  14602  bdel  14636  bdssex  14693  bj-indind  14723  findset  14736  nninfall  14797  trirec0  14831  neap0mkv  14856