Theorem sylibr 137

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

Hypotheses

Ref	Expression
sylibr.1	⊢ (φ → ψ)
sylibr.2	⊢ (χ ↔ ψ)

Assertion

Ref	Expression
sylibr	⊢ (φ → χ)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 ⊢ (φ → ψ)
2		sylibr.2	. . 3 ⊢ (χ ↔ ψ)
3	2	biimpri 124	. 2 ⊢ (ψ → χ)
4	1, 3	syl 14	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.74rd  172  bitri  173  3imtr4i  190  sylanbrc  394  dcimpstab  751  dcim  783  oibabs  799  stabtestimpdc  823  dcor  842  3mix1  1072  3mix2  1073  3jca  1083  syl3anbrc  1087  inegd  1262  pclem6  1264  xoranor  1267  nfxfrd  1361  nfd  1413  hban  1436  nfan1  1453  nford  1456  nfand  1457  hbim1  1459  alexim  1533  ax6blem  1537  nf4r  1558  19.34  1571  nfexd  1641  sbcof2  1688  nfsb2or  1715  sbidm  1728  nfdv  1754  nfeudv  1912  mon  1926  eumo  1929  mo23  1938  eu2  1941  eu3h  1942  exmodc  1947  exmonim  1948  mo2r  1949  mo3h  1950  bm1.1  2022  eqrdv  2035  3eltr4g  2120  abbi2dv  2153  abbi1dv  2154  nfcd  2170  nfcxfrd  2173  dcned  2209  3netr4g  2234  necon3bi  2249  necon2ai  2253  alral  2361  rspe  2364  rsp2e  2366  rgen2a  2369  ralrimi  2384  r19.27av  2442  r19.32r  2451  nfreudxy  2477  mormo  2515  nrexrmo  2520  cgsex2g  2584  cgsex4g  2585  spc2egv  2636  spc2gv  2637  spc3egv  2638  spc3gv  2639  rspce  2645  ceqex  2665  elrab3t  2691  mosubt  2712  mo2icl  2714  reu3  2725  reu6i  2726  2rmorex  2739  sbc5  2781  rspesbca  2836  rmo2ilem  2841  sbnfc2  2900  ssrd  2944  ssrdv  2945  3sstr4g  2980  syl5eqss  2983  ss2abdv  3007  abssdv  3008  rabssdv  3014  ss2rabdv  3015  ssun1  3100  unssad  3114  unssbd  3115  ssddif  3165  uneqin  3182  indifdir  3187  undif3ss  3192  reuss2  3211  n0rf  3227  reximdva0m  3230  rabxmdc  3243  ssindif0im  3275  minel  3277  ralidm  3315  ralm  3319  disjsn2  3424  absneu  3433  rabsneu  3434  opprc  3561  elunii  3576  dfnfc2  3589  uniss2  3602  unidif  3603  ssunieq  3604  intab  3635  iunss2  3693  iunxdif2  3696  invdisj  3750  3brtr4g  3787  trin  3855  triun  3858  truni  3859  trint  3860  iinexgm  3899  class2seteq  3907  pwuni  3934  mss  3953  copsex2t  3973  euotd  3982  pwunim  4014  ispod  4032  sotricim  4051  exse  4058  trssord  4083  suctr  4124  eusvnf  4151  eusvnfb  4152  eusv2nf  4154  rexxfrd  4161  ralxfr2d  4162  rexxfr2d  4163  rabxfrd  4167  reuhypd  4169  eldifpw  4174  iunpw  4177  ssorduni  4179  sucelon  4195  onsucelsucr  4199  sucunielr  4201  onsucelsucexmid  4215  setindel  4221  elirr  4224  en2lp  4232  suc11g  4235  ordsuc  4241  nlimsucg  4242  onpsssuc  4247  tfi  4248  peano5  4264  limom  4279  peano2b  4280  nndceq0  4282  eqrelrdv  4379  xpsspw  4393  relint  4404  relop  4429  eqbrrdva  4448  opeldm  4481  elres  4589  relssres  4591  exse2  4642  issref  4650  trin2  4659  dminss  4681  imainss  4682  rnxpid  4698  dmsn0el  4733  dmmptg  4761  relrelss  4787  cnviinm  4802  iotanul  4825  sniota  4837  dffun5r  4857  funmo  4860  funco  4883  funun  4887  funprg  4892  funtpg  4893  funtp  4895  fntpg  4898  fununi  4910  funcnvuni  4911  imadiflem  4921  imainlem  4923  funimaexglem  4925  isarep2  4929  fnunsn  4949  2elresin  4953  fnimadisj  4962  fco  4999  funssxp  5003  fssres  5009  feu  5015  fimacnvdisj  5017  fabexg  5020  f00  5024  f1co  5044  fores  5058  foco  5059  f1ores  5084  foimacnv  5087  f1oun  5089  fun11iun  5090  f1oco  5092  fo00  5105  brprcneu  5114  fv3  5140  relelfvdm  5148  nfvres  5149  nfunsn  5150  funfvbrb  5223  respreima  5238  dff2  5254  dff3im  5255  dffo4  5258  ffvresb  5271  f1oresrab  5272  fmptco  5273  fsn  5278  fpr  5288  ftpg  5290  fsnunf  5305  fsnunfv  5306  elabrex  5340  dff1o6  5359  foeqcnvco  5373  fliftel1  5377  isores1  5397  isoini2  5401  riotasbc  5426  acexmidlemph  5448  acexmidlemcase  5450  oprabidlem  5479  brabvv  5493  eloprabga  5533  fnoprabg  5544  caovimo  5636  oprabexd  5696  fo1stresm  5730  fo2ndresm  5731  unielxp  5742  1st2ndbr  5752  fmpt2co  5779  1stconst  5784  2ndconst  5785  poxp  5794  reldmtpos  5809  tposfun  5816  dftpos4  5819  smores  5848  smores2  5850  tfrlem1  5864  tfr0  5878  tfrlemibxssdm  5882  tfrlemibex  5884  tfrlemiubacc  5885  tfrlemi14d  5888  tfrexlem  5889  tfri1d  5890  tfri3  5894  2oconcl  5961  nnsucelsuc  6009  nntri3or  6011  nndceq  6015  nndcel  6016  ecexr  6047  brdifun  6069  ecelqsdm  6112  iinerm  6114  eroveu  6133  erovlem  6134  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  f1oen3g  6170  ssdomg  6194  domtr  6201  snfig  6227  nnfi  6251  dmaddpqlem  6361  nqpi  6362  dmaddpq  6363  dmmulpq  6364  ltdcnq  6381  subhalfnqq  6397  enq0sym  6414  enq0ref  6415  enq0tr  6416  nqnq0pi  6420  nq0nn  6424  addnq0mo  6429  mulnq0mo  6430  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  npsspw  6453  elnp1st2nd  6458  prnmaxl  6470  prnminu  6471  prarloc  6485  genprndl  6504  genprndu  6505  nqprm  6525  addnqpr1lemrl  6537  addnqpr1lemru  6538  prmuloc  6545  ltsopr  6568  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemopu  6575  recexprlemopl  6595  recexprlemopu  6597  recexprlemdisj  6600  archpr  6613  addsrmo  6631  mulsrmo  6632  recexgt0sr  6661  pitonn  6704  axaddcl  6710  axaddrcl  6711  axmulcl  6712  axmulrcl  6713  axrnegex  6723  axcnre  6725  axpre-lttrn  6728  axarch  6733  ltxrlt  6842  apirr  7349  rerecclap  7448  arch  7914  0mnnnnn0  7950  nnm1nn0  7959  elnnnn0c  7963  elnnz1  8004  ztri3or0  8023  nn0n0n1ge2  8047  zdceq  8052  zdcle  8053  zdclt  8054  uzind  8085  eluzge3nn  8250  eluz2b2  8276  elnn1uz2  8280  nn01to3  8288  znq  8295  qaddcl  8306  qmulcl  8308  qreccl  8311  irradd  8315  irrmul  8316  cnref1o  8317  iooidg  8508  elioo4g  8533  fzdcel  8634  fznlem  8635  fzpreddisj  8663  elfz0ubfz0  8712  elfz0fzfz0  8713  fz0fzelfz0  8714  fz0fzdiffz0  8717  elfzmlbp  8720  difelfzle  8722  4fvwrd4  8727  fzosplit  8763  elfzo0  8768  fzo1fzo0n0  8769  elfzonn0  8772  fzofzim  8774  elfzo1  8776  elfzom1elp1fzo  8788  fzossfzop1  8798  ssfzo12bi  8811  frec2uzrand  8832  frec2uzf1od  8833  frecuzrdgrom  8837  frecuzrdgfn  8839  frecfzennn  8844  expcl2lemap  8881  bj-nfalt  9173  bj-2inf  9326  peano5set  9328  bj-nntrans2  9340  bj-peano4  9343  bj-inf2vn  9358  bj-inf2vn2  9359  bj-findis  9363