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  6415  enq0ref  6416  enq0tr  6417  nqnq0pi  6421  nq0nn  6425  addnq0mo  6430  mulnq0mo  6431  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  npsspw  6454  elnp1st2nd  6459  prnmaxl  6471  prnminu  6472  prarloc  6486  genprndl  6504  genprndu  6505  nqprm  6525  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  prmuloc  6547  ltsopr  6570  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  recexprlemopl  6597  recexprlemopu  6599  recexprlemdisj  6602  archpr  6615  cauappcvgprlemdisj  6623  cauappcvgprlemladdrl  6629  cauappcvgprlem2  6632  caucvgprlemnbj  6638  caucvgprlemdisj  6645  caucvgprlemladdfu  6648  caucvgprlem2  6651  addsrmo  6671  mulsrmo  6672  recexgt0sr  6701  pitonn  6744  axaddcl  6750  axaddrcl  6751  axmulcl  6752  axmulrcl  6753  axrnegex  6763  axcnre  6765  axpre-lttrn  6768  axarch  6773  ltxrlt  6882  apirr  7389  rerecclap  7488  arch  7954  0mnnnnn0  7990  nnm1nn0  7999  elnnnn0c  8003  elnnz1  8044  ztri3or0  8063  nn0n0n1ge2  8087  zdceq  8092  zdcle  8093  zdclt  8094  uzind  8125  eluzge3nn  8290  eluz2b2  8316  elnn1uz2  8320  nn01to3  8328  znq  8335  qaddcl  8346  qmulcl  8348  qreccl  8351  irradd  8355  irrmul  8356  cnref1o  8357  iooidg  8548  elioo4g  8573  fzdcel  8674  fznlem  8675  fzpreddisj  8703  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbp  8760  difelfzle  8762  4fvwrd4  8767  fzosplit  8803  elfzo0  8808  fzo1fzo0n0  8809  elfzonn0  8812  fzofzim  8814  elfzo1  8816  elfzom1elp1fzo  8828  fzossfzop1  8838  ssfzo12bi  8851  frec2uzrand  8872  frec2uzf1od  8873  frecuzrdgrom  8877  frecuzrdgfn  8879  frecfzennn  8884  expcl2lemap  8921  rennim  9211  bj-nfalt  9239  bj-indind  9391  bj-2inf  9397  peano5setOLD  9400  bj-nntrans2  9412  bj-peano4  9415  bj-nnord  9418  bj-inf2vn  9434  bj-inf2vn2  9435  bj-findis  9439