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  396  dcimpstab  740  dcim  772  oibabs  788  stabtestimpdc  812  dcor  829  3mix1  1059  3mix2  1060  3jca  1067  syl3anbrc  1073  inegd  1246  pclem6  1248  xoranor  1251  nfxfrd  1340  nfd  1393  hban  1417  nfan1  1434  nford  1437  nfand  1438  hbim1  1440  alexim  1514  ax6blem  1518  nf4r  1539  19.34  1552  nfexd  1622  sbcof2  1669  nfsb2or  1696  sbidm  1709  nfdv  1735  nfeudv  1893  mon  1907  eumo  1910  mo23  1919  eu2  1922  eu3h  1923  exmodc  1928  exmonim  1929  mo2r  1930  mo3h  1931  bm1.1  2003  eqrdv  2016  3eltr4g  2101  abbi2dv  2134  abbi1dv  2135  nfcd  2151  nfcxfrd  2154  exmidnedc  2191  3netr4g  2214  necon3bi  2229  necon2ai  2233  alral  2341  rspe  2344  rsp2e  2346  rgen2a  2349  ralrimi  2364  r19.27av  2422  r19.32r  2431  nfreudxy  2457  mormo  2495  nrexrmo  2500  cgsex2g  2563  cgsex4g  2564  spc2egv  2615  spc2gv  2616  spc3egv  2617  spc3gv  2618  rspce  2624  ceqex  2644  elrab3t  2670  mosubt  2691  mo2icl  2693  reu3  2704  reu6i  2705  2rmorex  2718  sbc5  2760  rspesbca  2815  rmo2ilem  2820  sbnfc2  2879  ssrd  2923  ssrdv  2924  3sstr4g  2959  syl5eqss  2962  ss2abdv  2986  abssdv  2987  rabssdv  2993  ss2rabdv  2994  ssun1  3079  unssad  3093  unssbd  3094  ssddif  3144  uneqin  3161  indifdir  3166  undif3ss  3171  reuss2  3190  n0rf  3206  reximdva0m  3209  rabxmdc  3222  ssindif0im  3254  minel  3256  ralidm  3296  ralm  3300  disjsn2  3403  absneu  3412  rabsneu  3413  opprc  3540  elunii  3555  dfnfc2  3568  uniss2  3581  unidif  3582  ssunieq  3583  intab  3614  iunss2  3672  iunxdif2  3675  invdisj  3729  3brtr4g  3766  trin  3834  triun  3837  truni  3838  trint  3839  iinexgm  3878  class2seteq  3886  pwuni  3913  mss  3932  copsex2t  3952  euotd  3961  pwunim  3993  ispod  4011  sotricim  4030  exse  4037  trssord  4062  suctrALT  4103  eusvnf  4131  eusvnfb  4132  eusv2nf  4134  rexxfrd  4141  ralxfr2d  4142  rexxfr2d  4143  rabxfrd  4147  reuhypd  4149  eldifpw  4154  iunpw  4157  ssorduni  4159  sucelon  4175  onsucelsucr  4179  sucunielr  4181  onsucelsucexmid  4195  setindel  4201  elirr  4204  en2lp  4212  suc11g  4215  ordsuc  4221  nlimsucg  4222  onpsssuc  4227  tfi  4228  peano5  4244  limom  4259  peano2b  4260  nndceq0  4262  eqrelrdv  4359  xpsspw  4373  relint  4384  relop  4409  eqbrrdva  4428  opeldm  4461  elres  4569  relssres  4571  exse2  4622  issref  4630  trin2  4639  dminss  4661  imainss  4662  rnxpid  4678  dmsn0el  4713  dmmptg  4741  relrelss  4767  cnviinm  4782  iotanul  4805  sniota  4817  funmo  4839  funco  4862  funun  4866  funprg  4871  funtpg  4872  funtp  4874  fntpg  4877  fununi  4889  funcnvuni  4890  imadiflem  4900  imainlem  4902  funimaexglem  4904  isarep2  4908  fnunsn  4928  2elresin  4932  fnimadisj  4941  fco  4977  funssxp  4981  fssres  4987  feu  4993  fimacnvdisj  4995  fabexg  4998  f00  5002  f1co  5022  fores  5036  foco  5037  f1ores  5062  foimacnv  5065  f1oun  5067  fun11iun  5068  f1oco  5070  fo00  5083  brprcneu  5092  fv3  5118  relelfvdm  5126  nfvres  5127  nfunsn  5128  funfvbrb  5201  respreima  5216  dff2  5232  dff3im  5233  dffo4  5236  ffvresb  5249  f1oresrab  5250  fmptco  5251  fsn  5256  fpr  5266  ftpg  5268  fsnunf  5283  fsnunfv  5284  elabrex  5318  dff1o6  5337  foeqcnvco  5351  fliftel1  5355  isores1  5375  isoini2  5379  riotasbc  5403  acexmidlemph  5425  acexmidlemcase  5427  oprabidlem  5456  brabvv  5470  eloprabga  5510  fnoprabg  5521  caovimo  5613  oprabexd  5673  fo1stresm  5707  fo2ndresm  5708  unielxp  5719  1st2ndbr  5729  fmpt2co  5756  1stconst  5761  2ndconst  5762  poxp  5771  reldmtpos  5786  tposfun  5793  dftpos4  5796  smores  5825  smores2  5827  tfrlem1  5841  tfrlemibxssdm  5858  tfrlemibex  5860  tfrlemiubacc  5861  tfrlemi14d  5864  tfrlemi14  5865  tfrexlem  5866  tfri1d  5867  tfri3  5871  2oconcl  5933  nnsucelsuc  5981  nntri3or  5983  nndceq  5986  nndcel  5987  ecexr  6018  brdifun  6040  ecelqsdm  6083  iinerm  6085  eroveu  6104  erovlem  6105  ecopovtrn  6110  ecopovtrng  6113  th3qlem1  6115  dmaddpqlem  6230  nqpi  6231  dmaddpq  6232  dmmulpq  6233  ltdcnq  6250  subhalfnqq  6265  enq0sym  6281  enq0ref  6282  enq0tr  6283  nqnq0pi  6287  nq0nn  6291  addnq0mo  6296  mulnq0mo  6297  nqpnq0nq  6302  nqnq0a  6303  nqnq0m  6304  npsspw  6319  elnp1st2nd  6324  prnmaxl  6336  prnminu  6337  prarloc  6351  genprndl  6370  genprndu  6371  nqprm  6391  prmuloc  6404  ltsopr  6427  ltexprlemm  6431  ltexprlemopl  6432  ltexprlemopu  6434  recexprlemopl  6453  recexprlemopu  6455  recexprlemdisj  6458  addsrmo  6484  mulsrmo  6485  axaddcl  6554  axaddrcl  6555  axmulcl  6556  axmulrcl  6557  axrnegex  6567  axcnre  6569  axpre-lttrn  6572  ltxrlt  6680  bj-nfalt  7150  bj-2inf  7299  peano5set  7301  bj-nntrans2  7313  bj-peano4  7316  bj-inf2vn  7331  bj-inf2vn2  7332  bj-findis  7336