Theorem sylibr 133

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 132	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbbr  135  pm5.74rd  182  bitri  183  3imtr4i  200  sylanbrc  413  oibabs  703  dcim  826  dcstab  829  stdcndc  830  stdcndcOLD  831  dcor  919  3mix1  1150  3mix2  1151  3jca  1161  syl3anbrc  1165  inegd  1350  pclem6  1352  xoranor  1355  nfxfrd  1451  nfd  1503  hban  1526  nfan1  1543  nford  1546  nfand  1547  hbim1  1549  alexim  1624  ax6blem  1628  nf4r  1649  19.34  1662  nfexd  1734  sbcof2  1782  nfsb2or  1809  sbidm  1823  nfdv  1849  nfeudv  2014  mon  2028  eumo  2031  mo23  2040  eu2  2043  eu3h  2044  exmodc  2049  exmonim  2050  mo2r  2051  mo3h  2052  bm1.1  2124  eqrdv  2137  3eltr4g  2225  abbi2dv  2258  abbi1dv  2259  nfcd  2276  nfcxfrd  2279  dcned  2314  neqned  2315  3netr4g  2343  necon3bi  2358  necon2ai  2362  alral  2478  rspe  2481  rsp2e  2483  rgen2a  2486  ralrimi  2503  r19.27v  2559  r19.28v  2560  r19.27av  2567  r19.32r  2578  nfreudxy  2604  mormo  2642  nrexrmo  2647  cgsex2g  2722  cgsex4g  2723  spc2egv  2775  spc2gv  2776  spc3egv  2777  spc3gv  2778  rspce  2784  ceqex  2812  elrab3t  2839  elrabd  2842  mosubt  2861  mo2icl  2863  reu3  2874  reu6i  2875  2rmorex  2890  sbc5  2932  rspesbca  2993  rmo2ilem  2998  sbnfc2  3060  ssrd  3102  ssrdv  3103  3sstr4g  3140  eqsstrid  3143  ss2abdv  3170  abssdv  3171  rabssdv  3177  ss2rabdv  3178  ssun1  3239  unssad  3253  unssbd  3254  ssddif  3310  uneqin  3327  indifdir  3332  undif3ss  3337  reuss2  3356  n0rf  3375  reximdva0m  3378  rabxmdc  3394  ssindif0im  3422  minel  3424  ralidm  3463  ralm  3467  dcun  3473  ifmdc  3509  disjsn2  3586  absneu  3595  rabsneu  3596  opprc  3726  elunii  3741  dfnfc2  3754  uniss2  3767  unidif  3768  ssunieq  3769  intab  3800  iunss2  3858  iunxdif2  3861  invdisj  3923  disjiun  3924  3brtr4g  3962  trin  4036  triun  4039  truni  4040  trint  4041  iinexgm  4079  class2seteq  4087  pwuni  4116  exmid1dc  4123  exmidn0m  4124  exmidsssn  4125  exmid0el  4127  exmidel  4128  exmidundif  4129  exmidundifim  4130  mss  4148  copsex2t  4167  euotd  4176  pwunim  4208  ispod  4226  sotricim  4245  exse  4258  frind  4274  trssord  4302  suctr  4343  pwnex  4370  eusvnf  4374  eusvnfb  4375  eusv2nf  4377  rexxfrd  4384  ralxfr2d  4385  rexxfr2d  4386  rabxfrd  4390  reuhypd  4392  eldifpw  4398  iunpw  4401  ssorduni  4403  sucelon  4419  onsucelsucr  4424  sucunielr  4426  ordtri2or2exmidlem  4441  onsucelsucexmid  4445  reg2exmidlema  4449  setindel  4453  elirr  4456  orddisj  4461  en2lp  4469  suc11g  4472  ordsuc  4478  nlimsucg  4481  ordtri2or2exmid  4486  zfregfr  4488  wessep  4492  tfi  4496  peano5  4512  limom  4527  peano2b  4528  nndceq0  4531  nnpredcl  4536  0nelrel  4585  eqrelrdv  4635  xpsspw  4651  relint  4663  relop  4689  eqbrrdva  4709  opeldm  4742  elres  4855  relssres  4857  exse2  4913  issref  4921  trin2  4930  dminss  4953  imainss  4954  rnxpid  4973  dmsn0el  5008  dmmptg  5036  relrelss  5065  cnviinm  5080  iotanul  5103  sniota  5115  dffun5r  5135  funmo  5138  funco  5163  funun  5167  funprg  5173  funtpg  5174  funtp  5176  fntpg  5179  fununi  5191  funcnvuni  5192  imadiflem  5202  imainlem  5204  funimaexglem  5206  isarep2  5210  fnunsn  5230  2elresin  5234  fnimadisj  5243  dmmptd  5253  fco  5288  funssxp  5292  fssres  5298  feu  5305  fimacnvdisj  5307  fabexg  5310  f00  5314  f0rn0  5317  f1co  5340  fores  5354  foco  5355  f1ores  5382  foimacnv  5385  f1oun  5387  fun11iun  5388  f1oco  5390  fo00  5403  brprcneu  5414  fv3  5444  relelfvdm  5453  nfvres  5454  nfunsn  5455  funfvbrb  5533  respreima  5548  dff2  5564  dff3im  5565  dffo4  5568  fvmptelrn  5573  ffvresb  5583  f1oresrab  5585  fmptco  5586  fsn  5592  fpr  5602  ftpg  5604  fsnunf  5620  fsnunfv  5621  elabrex  5659  dff1o6  5677  foeqcnvco  5691  fliftel1  5695  isores1  5715  isoini2  5720  riotasbc  5745  acexmidlemph  5767  acexmidlemcase  5769  oprabidlem  5802  brabvv  5817  eloprabga  5858  fnoprabg  5872  caovimo  5964  oprabexd  6025  fo1stresm  6059  fo2ndresm  6060  unielxp  6072  1st2ndbr  6082  fmpoco  6113  1stconst  6118  2ndconst  6119  poxp  6129  spc2ed  6130  disjxp1  6133  reldmtpos  6150  tposfun  6157  dftpos4  6160  smores  6189  smores2  6191  tfrlem1  6205  tfr0dm  6219  tfrlemibxssdm  6224  tfrlemibex  6226  tfrlemiubacc  6227  tfrlemi14d  6230  tfrexlem  6231  tfri1d  6232  tfr1onlembxssdm  6240  tfr1onlembex  6242  tfr1onlemubacc  6243  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllembxssdm  6253  tfrcllembex  6255  tfrcllemubacc  6256  tfrcllemres  6259  tfri3  6264  rdgon  6283  frecabcl  6296  frecfcllem  6301  frecrdg  6305  2oconcl  6336  nnsucelsuc  6387  nntri3or  6389  nndceq  6395  nndcel  6396  dcdifsnid  6400  ecexr  6434  brdifun  6456  ecelqsdm  6499  iinerm  6501  eroveu  6520  erovlem  6521  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  pmsspw  6577  map0b  6581  mapsn  6584  mapsncnv  6589  ixpf  6614  uniixp  6615  ixpexgg  6616  resixp  6627  f1oen3g  6648  ssdomg  6672  domtr  6679  snfig  6708  enpr2d  6711  xpf1o  6738  xpmapenlem  6743  php5dom  6757  fidceq  6763  nnfi  6766  fiunsnnn  6775  findcard  6782  findcard2  6783  findcard2s  6784  ac6sfi  6792  tridc  6793  fimax2gtri  6795  finexdc  6796  exmidpw  6802  nnwetri  6804  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  tpfidisj  6816  iunfidisj  6834  snexxph  6838  fidcenumlemrks  6841  sbthlem2  6846  sbthlemi3  6847  sbthlem7  6851  sbthlemi8  6852  fival  6858  supmoti  6880  djuss  6955  updjudhf  6964  updjud  6967  casefun  6970  caseinj  6974  omp1eomlem  6979  djufun  6989  djuinj  6991  ctssdccl  6996  ctfoex  7003  finomni  7012  exmidomniim  7013  exmidomni  7014  fodjuomnilemdc  7016  nnnninf  7023  exmidonfinlem  7049  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  dju1en  7069  dmaddpqlem  7185  nqpi  7186  dmaddpq  7187  dmmulpq  7188  ltdcnq  7205  subhalfnqq  7222  enq0sym  7240  enq0ref  7241  enq0tr  7242  nqnq0pi  7246  nq0nn  7250  addnq0mo  7255  mulnq0mo  7256  nqpnq0nq  7261  nqnq0a  7262  nqnq0m  7263  npsspw  7279  elnp1st2nd  7284  prnmaxl  7296  prnminu  7297  prarloc  7311  genprndl  7329  genprndu  7330  nqprm  7350  nqprl  7359  nqpru  7360  addnqprlemrl  7365  addnqprlemru  7366  prmuloc  7374  mulnqprlemrl  7381  mulnqprlemru  7382  ltsopr  7404  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  lteupri  7425  recexprlemopl  7433  recexprlemopu  7435  recexprlemdisj  7438  archpr  7451  cauappcvgprlemdisj  7459  cauappcvgprlemladdrl  7465  cauappcvgprlem2  7468  caucvgprlemnbj  7475  caucvgprlemdisj  7482  caucvgprlemladdfu  7485  caucvgprlem2  7488  caucvgprprlemnbj  7501  caucvgprprlemdisj  7510  suplocexprlemml  7524  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemloc  7529  addsrmo  7551  mulsrmo  7552  recexgt0sr  7581  prsrpos  7593  caucvgsrlemasr  7598  suplocsrlemb  7614  suplocsrlempr  7615  suplocsr  7617  elrealeu  7637  pitonn  7656  pitoregt0  7657  pitore  7658  recnnre  7659  axaddcl  7672  axaddrcl  7673  axmulcl  7674  axmulrcl  7675  axrnegex  7687  axcnre  7689  axpre-lttrn  7692  rereceu  7697  axarch  7699  axpre-suploclemres  7709  axpre-suploc  7710  ltxrlt  7830  apirr  8367  cnstab  8407  divmulasscomap  8456  rerecclap  8490  lbreu  8703  arch  8974  0mnnnnn0  9009  nnm1nn0  9018  elnnnn0c  9022  elnnz1  9077  ztri3or0  9096  nzadd  9106  nn0n0n1ge2  9121  zdceq  9126  zdcle  9127  zdclt  9128  uzind  9162  eluzge3nn  9367  supinfneg  9390  infsupneg  9391  eluz2b2  9397  elnn1uz2  9401  nn01to3  9409  znq  9416  qaddcl  9427  qmulcl  9429  qreccl  9434  irradd  9438  irrmul  9439  cnref1o  9440  xrpnfdc  9625  xrmnfdc  9626  xaddcom  9644  xnegdi  9651  xpncan  9654  xleadd1a  9656  iooidg  9692  elioo4g  9717  fzdcel  9820  fznlem  9821  fzpreddisj  9851  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  fz0fzdiffz0  9907  elfzmlbp  9909  difelfzle  9911  4fvwrd4  9917  fzosplit  9954  elfzo0  9959  fzo1fzo0n0  9960  elfzonn0  9963  fzofzim  9965  elfzo1  9967  elfzom1elp1fzo  9979  fzossfzop1  9989  ssfzo12bi  10002  exfzdc  10017  qdceq  10024  exbtwnzlemstep  10025  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnxr  10035  modfzo0difsn  10168  frec2uzrand  10178  frec2uzf1od  10179  frecuzrdgrcl  10183  frecuzrdgtcl  10185  frecuzrdgrclt  10188  frecuzrdgfunlem  10192  frecfzennn  10199  seq3f1olemp  10275  seq3f1oleml  10276  ser0f  10288  expcl2lemap  10305  hashunsng  10553  shftfvalg  10590  shftfval  10593  caucvgre  10753  rexanuz  10760  recvguniq  10767  rennim  10774  resqrexlemf  10779  rsqrmo  10799  fimaxre2  10998  climeu  11065  sumdc  11127  summodc  11152  zsumdc  11153  isum  11154  fisumss  11161  isumss2  11162  fsumsplit  11176  sumsnf  11178  fsumsplitsn  11179  sumtp  11183  sumsplitdc  11201  fsum2dlemstep  11203  fisum0diag2  11216  fsumconst  11223  modfsummodlemstep  11226  fsum00  11231  fsumabs  11234  fsumiun  11246  isumlessdc  11265  expcnv  11273  prodmodc  11347  ef0lem  11366  modmulconst  11525  dvdsdivcl  11548  dvdsssfz1  11550  dvdsfac  11558  zeoxor  11566  nn0ehalf  11600  nn0oddm1d2  11606  nnoddm1d2  11607  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemstep  11638  infssuzex  11642  gcdsupex  11646  gcdsupcl  11647  bezoutlemnewy  11684  bezoutlemmain  11686  bezoutlemeu  11695  dfgcd2  11702  algrf  11726  algcvgblem  11730  lcmgcdlem  11758  lcmdvds  11760  coprmgcdb  11769  mulgcddvds  11775  qredeu  11778  cncongr1  11784  cncongr2  11785  isprm2lem  11797  dvdsnprmd  11806  oddprmge3  11815  pw2dvdseu  11846  phibndlem  11892  dfphi2  11896  hashdvds  11897  phiprmpw  11898  hashgcdeq  11904  ennnfonelemdc  11912  ennnfonelemh  11917  ennnfonelemhf1o  11926  ennnfonelemf1  11931  ennnfonelemrn  11932  ennnfonelemdm  11933  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctiunctlemudc  11950  ctiunctlemf  11951  isstructim  11973  setsresg  11997  strleund  12047  1strbas  12058  2strbasg  12060  2stropg  12061  restsspw  12130  istopon  12180  toponcom  12194  topgele  12196  topontopn  12204  tsettps  12205  tgval  12218  eltg2b  12223  unitg  12231  tgss2  12248  bastop2  12253  distop  12254  epttop  12259  cldss2  12275  neisspw  12317  neipsm  12323  neiuni  12330  tgcn  12377  tgcnp  12378  cnntr  12394  lmff  12418  txuni2  12425  txbasex  12426  txbas  12427  txcnp  12440  txcnmpt  12442  txcn  12444  txdis  12446  txdis1cn  12447  cnmpt11  12452  cnmpt12  12456  cnmpt21  12460  cnmpt2t  12462  cnmpt22  12463  blsscls2  12662  xmetxpbl  12677  xmettxlem  12678  tgqioo  12716  fsumcncntop  12725  cncfmpt1f  12753  mulcncflem  12759  mulcncf  12760  dedekindeu  12770  dedekindicclemicc  12779  dedekindicc  12780  ivthinclemdisj  12787  limcimo  12803  cnmptlimc  12812  reldvg  12817  dvfvalap  12819  dvfgg  12826  dveflem  12855  dvef  12856  sincn  12858  coscn  12859  pilem3  12864  bj-nnal  12949  bj-trst  12951  bj-fast  12952  bj-stand  12956  bj-trdc  12959  bj-fadc  12960  decidr  13003  djulclALT  13008  djurclALT  13009  bj-indind  13130  bj-2inf  13136  bj-nntrans2  13150  bj-peano4  13153  bj-nnord  13156  bj-inf2vn  13172  bj-inf2vn2  13173  bj-findis  13177  pwf1oexmid  13194  exmid1stab  13195  subctctexmid  13196  nnsf  13199  nninfsellemdc  13206  nninffeq  13216  exmidsbthrlem  13217  sbthom  13221  triap  13224  trilpo  13236