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  6503  genprndu  6504  nqprm  6524  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  prmuloc  6546  ltsopr  6569  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  recexprlemopl  6596  recexprlemopu  6598  recexprlemdisj  6601  archpr  6614  cauappcvgprlemdisj  6622  cauappcvgprlemladdrl  6628  cauappcvgprlem2  6631  addsrmo  6651  mulsrmo  6652  recexgt0sr  6681  pitonn  6724  axaddcl  6730  axaddrcl  6731  axmulcl  6732  axmulrcl  6733  axrnegex  6743  axcnre  6745  axpre-lttrn  6748  axarch  6753  ltxrlt  6862  apirr  7369  rerecclap  7468  arch  7934  0mnnnnn0  7970  nnm1nn0  7979  elnnnn0c  7983  elnnz1  8024  ztri3or0  8043  nn0n0n1ge2  8067  zdceq  8072  zdcle  8073  zdclt  8074  uzind  8105  eluzge3nn  8270  eluz2b2  8296  elnn1uz2  8300  nn01to3  8308  znq  8315  qaddcl  8326  qmulcl  8328  qreccl  8331  irradd  8335  irrmul  8336  cnref1o  8337  iooidg  8528  elioo4g  8553  fzdcel  8654  fznlem  8655  fzpreddisj  8683  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzmlbp  8740  difelfzle  8742  4fvwrd4  8747  fzosplit  8783  elfzo0  8788  fzo1fzo0n0  8789  elfzonn0  8792  fzofzim  8794  elfzo1  8796  elfzom1elp1fzo  8808  fzossfzop1  8818  ssfzo12bi  8831  frec2uzrand  8852  frec2uzf1od  8853  frecuzrdgrom  8857  frecuzrdgfn  8859  frecfzennn  8864  expcl2lemap  8901  rennim  9191  bj-nfalt  9219  bj-2inf  9372  peano5set  9374  bj-nntrans2  9386  bj-peano4  9389  bj-inf2vn  9404  bj-inf2vn2  9405  bj-findis  9409