Theorem sylibr 134

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbbr  136  pm5.74rd  183  bitri  184  3imtr4i  201  sylanbrc  417  mpnanrd  699  oibabs  721  dcim  848  dcstab  851  stdcndc  852  stdcndcOLD  853  dcand  940  dcor  943  dfifp2dc  989  3mix1  1192  3mix2  1193  3jca  1203  syl3anbrc  1207  syl21anbrc  1208  inegd  1416  pclem6  1418  xoranor  1421  dcfrompeirce  1494  nfxfrd  1523  nfd  1571  hban  1595  nfan1  1612  nford  1615  nfand  1616  hbim1  1618  nfal  1624  alexim  1693  nnal  1697  ax6blem  1698  nf4r  1719  19.34  1732  nfexd  1809  sbcof2  1858  nfsb2or  1885  sbidm  1899  nfdv  1925  nfd2  2075  nfeudv  2094  mon  2108  eumo  2111  mo23  2121  eu2  2124  eu3h  2125  exmodc  2130  exmonim  2131  mo2r  2132  mo3h  2133  bm1.1  2216  eqrdv  2229  3eltr4g  2317  abbi2dv  2350  abbi1dv  2351  nfcd  2369  nfcxfrd  2372  dcned  2408  neqned  2409  3netr4g  2437  necon3bi  2452  necon2ai  2456  nnral  2522  alral  2577  rspe  2581  rsp2e  2583  rgen2a  2586  ralrimi  2603  r19.27v  2660  r19.28v  2661  r19.27av  2668  r19.32r  2679  nfreudxy  2707  mormo  2750  nrexrmo  2755  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc2gv  2897  spc3egv  2898  spc3gv  2899  rspce  2905  ceqex  2933  elrab3t  2961  elrabd  2964  mosubt  2983  mo2icl  2985  reu3  2996  reu6i  2997  2rmorex  3012  sbc5  3055  rspesbca  3117  rmo2ilem  3122  sbnfc2  3188  ssrd  3232  ssrdv  3233  3sstr4g  3270  eqsstrid  3273  ss2abdv  3300  abssdv  3301  rabssdv  3307  ss2rabdv  3308  ssun1  3370  unssad  3384  unssbd  3385  ssddif  3441  uneqin  3458  indifdir  3463  undif3ss  3468  reuss2  3487  n0rf  3507  reximdva0m  3510  rabxmdc  3526  ssindif0im  3554  minel  3556  ralidm  3595  ralm  3598  dcun  3604  ifmdc  3648  disjsn2  3732  rabsnif  3738  absneu  3743  rabsneu  3744  opprc  3883  elunii  3898  dfnfc2  3911  uniss2  3924  unidif  3925  ssunieq  3926  intab  3957  iunss2  4015  iunssd  4016  iunxdif2  4019  invdisj  4081  disjiun  4083  3brtr4g  4122  trin  4197  triun  4200  truni  4201  trint  4202  iinexgm  4244  class2seteq  4253  pwuni  4282  exmid1dc  4290  exmidn0m  4291  exmidsssn  4292  exmid0el  4294  exmidel  4295  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  mss  4318  copsex2t  4337  euotd  4347  pwunim  4383  ispod  4401  sotricim  4420  exse  4433  frind  4449  trssord  4477  suctr  4518  pwnex  4546  eusvnf  4550  eusvnfb  4551  eusv2nf  4553  rexxfrd  4560  ralxfr2d  4561  rexxfr2d  4562  rabxfrd  4566  reuhypd  4568  eldifpw  4574  iunpw  4577  ssorduni  4585  onsucb  4601  onsucelsucr  4606  sucunielr  4608  ontriexmidim  4620  ordtri2or2exmidlem  4624  onsucelsucexmid  4628  reg2exmidlema  4632  setindel  4636  elirr  4639  orddisj  4644  en2lp  4652  suc11g  4655  ordsuc  4661  nlimsucg  4664  ordtri2or2exmid  4669  ontri2orexmidim  4670  zfregfr  4672  wessep  4676  tfi  4680  peano5  4696  limom  4712  peano2b  4713  nndceq0  4716  nnpredcl  4721  0nelrel  4772  eqrelrdv  4822  xpsspw  4838  relint  4851  relop  4880  eqbrrdva  4900  ssrelrn  4922  opeldm  4934  reldmm  4950  elres  5049  relssres  5051  elrelimasn  5102  exse2  5110  issref  5119  trin2  5128  dminss  5151  imainss  5152  rnxpid  5171  dmsn0el  5206  dmmptg  5234  relrelss  5263  cnviinm  5278  iotanul  5302  sniota  5317  dffun5r  5338  funmo  5341  funco  5366  funun  5371  fununmo  5372  fununfun  5373  funprg  5380  funtpg  5381  funtp  5383  fntpg  5386  fununi  5398  funcnvuni  5399  imadiflem  5409  imainlem  5411  funimaexglem  5413  isarep2  5417  fnunsn  5439  2elresin  5443  fnimadisj  5453  dmmptd  5463  fco  5500  funssxp  5504  fssres  5512  feu  5519  fimacnvdisj  5521  fabexg  5524  f00  5528  f0rn0  5531  f1co  5554  fores  5569  foco  5570  f1ores  5598  foimacnv  5601  f1oun  5603  fun11iun  5604  f1oco  5606  fo00  5621  brprcneu  5632  fv3  5662  relelfvdm  5671  nfvres  5675  nfunsn  5676  funfvbrb  5760  respreima  5775  dff2  5791  dff3im  5792  dffo4  5795  fvmptelcdm  5800  ffvresb  5810  f1oresrab  5812  fmptco  5813  fsn  5819  fcof  5833  fpr  5836  ftpg  5838  fsnunf  5854  fsnunfv  5855  elabrex  5898  dff1o6  5917  foeqcnvco  5931  fliftel1  5935  isores1  5955  isoini2  5960  riotasbc  5988  acexmidlemph  6011  acexmidlemcase  6013  oprabidlem  6049  brabvv  6067  eloprabga  6108  fnoprabg  6122  caovimo  6216  oprabexd  6289  uchoice  6300  fo1stresm  6324  fo2ndresm  6325  unielxp  6337  1st2ndbr  6347  opabn1stprc  6358  fmpoco  6381  1stconst  6386  2ndconst  6387  poxp  6397  spc2ed  6398  disjxp1  6401  elmpom  6403  reldmtpos  6419  tposfun  6426  dftpos4  6429  smores  6458  smores2  6460  tfrlem1  6474  tfr0dm  6488  tfrlemibxssdm  6493  tfrlemibex  6495  tfrlemiubacc  6496  tfrlemi14d  6499  tfrexlem  6500  tfri1d  6501  tfr1onlembxssdm  6509  tfr1onlembex  6511  tfr1onlemubacc  6512  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllembxssdm  6522  tfrcllembex  6524  tfrcllemubacc  6525  tfrcllemres  6528  tfri3  6533  rdgon  6552  frecabcl  6565  frecfcllem  6570  frecrdg  6574  2oconcl  6607  nnsucelsuc  6659  nntri3or  6661  nndceq  6667  nndcel  6668  dcdifsnid  6672  ecexr  6707  brdifun  6729  ecelqsdm  6774  iinerm  6776  eroveu  6795  erovlem  6796  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  pmsspw  6852  map0b  6856  mapsn  6859  mapsncnv  6864  ixpf  6889  uniixp  6890  ixpexgg  6891  resixp  6902  f1oen3g  6927  ssdomg  6952  domtr  6959  snfig  6989  modom  6994  enpr2d  6997  dom1o  7002  xpf1o  7030  xpmapenlem  7035  php5dom  7049  fidceq  7056  nnfi  7059  fiunsnnn  7070  findcard  7077  findcard2  7078  findcard2s  7079  ac6sfi  7087  fidcen  7088  tridc  7089  fimax2gtri  7091  finexdc  7092  elssdc  7094  eqsndc  7095  exmidpw  7100  exmidpweq  7101  exmidpw2en  7104  nnwetri  7108  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  tpfidisj  7121  tpfidceq  7122  exmidssfi  7131  iunfidisj  7145  snexxph  7149  fidcenumlemrks  7152  sbthlem2  7157  sbthlemi3  7158  sbthlem7  7162  sbthlemi8  7163  fival  7169  dcfi  7180  supmoti  7192  djuss  7269  updjudhf  7278  updjud  7281  casefun  7284  caseinj  7288  omp1eomlem  7293  djufun  7303  djuinj  7305  ctssdccl  7310  ctfoex  7317  nnnninf  7325  nnnninfeq2  7328  nninfisollem0  7329  nninfisollemne  7330  nninfisollemeq  7331  nninfisol  7332  finomni  7339  exmidomniim  7340  exmidomni  7341  fodjuomnilemdc  7343  omniwomnimkv  7366  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoim  7378  nninfinfwlpo  7379  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  finacn  7419  exmidaclem  7423  dju1en  7428  exmidontriimlem1  7436  exmidontriimlem3  7438  iftrueb01  7441  pw1on  7444  3nsssucpw1  7454  2omotaplemap  7476  2omotap  7478  exmidmotap  7480  cc4f  7488  cc4n  7490  acnccim  7491  dmaddpqlem  7597  nqpi  7598  dmaddpq  7599  dmmulpq  7600  ltdcnq  7617  subhalfnqq  7634  enq0sym  7652  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nq0nn  7662  addnq0mo  7667  mulnq0mo  7668  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  npsspw  7691  elnp1st2nd  7696  prnmaxl  7708  prnminu  7709  prarloc  7723  genprndl  7741  genprndu  7742  nqprm  7762  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  prmuloc  7786  mulnqprlemrl  7793  mulnqprlemru  7794  ltsopr  7816  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  lteupri  7837  recexprlemopl  7845  recexprlemopu  7847  recexprlemdisj  7850  archpr  7863  cauappcvgprlemdisj  7871  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemnbj  7887  caucvgprlemdisj  7894  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemnbj  7913  caucvgprprlemdisj  7922  suplocexprlemml  7936  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemloc  7941  addsrmo  7963  mulsrmo  7964  recexgt0sr  7993  prsrpos  8005  caucvgsrlemasr  8010  suplocsrlemb  8026  suplocsrlempr  8027  suplocsr  8029  elrealeu  8049  pitonn  8068  pitoregt0  8069  pitore  8070  recnnre  8071  axaddcl  8084  axaddrcl  8085  axmulcl  8086  axmulrcl  8087  axrnegex  8099  axcnre  8101  axpre-lttrn  8104  rereceu  8109  axarch  8111  axpre-suploclemres  8121  axpre-suploc  8122  ltxrlt  8245  apirr  8785  divmulasscomap  8876  rerecclap  8910  lbreu  9125  arch  9399  0mnnnnn0  9434  nnm1nn0  9443  elnnnn0c  9447  elnnz1  9502  ztri3or0  9521  nzadd  9532  nn0n0n1ge2  9550  zdceq  9555  zdcle  9556  zdclt  9557  uzind  9591  eluzge3nn  9806  supinfneg  9829  infsupneg  9830  eluz2b2  9837  elnn1uz2  9841  elnn0dc  9845  elnndc  9846  nn01to3  9851  znq  9858  qaddcl  9869  qmulcl  9871  qreccl  9876  irradd  9880  irrmul  9881  elpq  9883  cnref1o  9885  xnn0dcle  10037  xrpnfdc  10077  xrmnfdc  10078  xaddcom  10096  xnegdi  10103  xpncan  10106  xleadd1a  10108  iooidg  10144  elioo4g  10169  elfzd  10251  fzdcel  10275  fznlem  10276  fzpreddisj  10306  fz0to4untppr  10359  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  4fvwrd4  10375  fzosplit  10414  elfzo0  10421  nn0p1elfzo  10422  fzo1fzo0n0  10423  elfzonn0  10426  fzofzim  10428  elfzo1  10431  elfzom1elp1fzo  10448  fzossfzop1  10458  ssfzo12bi  10471  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  qdceq  10505  qdclt  10506  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnxr  10518  modfzo0difsn  10658  frec2uzrand  10668  frec2uzf1od  10669  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgrclt  10678  frecuzrdgfunlem  10682  frecfzennn  10689  nninfinf  10706  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem1  10782  ser0f  10797  expcl2lemap  10814  hashunsng  11072  iswrdinn0  11119  snopiswrd  11124  wrdlndm  11131  iswrdsymb  11132  wrdsymb1  11151  ccatfv0  11181  ccatval21sw  11183  lswccatn0lsw  11189  eqs1  11206  ccat1st1st  11219  lswccats1fst  11222  fzowrddc  11229  swrdfv0  11236  swrdlen2  11244  swrdfv2  11245  swrdsbslen  11248  swrdspsleq  11249  pfxfv0  11274  pfxtrcfv0  11276  pfxeq  11278  pfx1  11285  swrdswrdlem  11286  cats1un  11303  pfxccatin12lem2a  11309  pfxccatin12lem2  11313  pfxccatin12lem3  11314  swrdccat  11317  cats1fvn  11346  cats1fvnd  11347  shftfvalg  11380  shftfval  11383  caucvgre  11543  rexanuz  11550  recvguniq  11557  rennim  11564  resqrexlemf  11569  rsqrmo  11589  fimaxre2  11789  climeu  11858  sumdc  11920  summodc  11946  zsumdc  11947  isum  11948  fisumss  11955  isumss2  11956  fsumsplit  11970  sumsnf  11972  fsumsplitsn  11973  sumtp  11977  sumsplitdc  11995  fsum2dlemstep  11997  fisum0diag2  12010  fsumconst  12017  modfsummodlemstep  12020  fsum00  12025  fsumabs  12028  fsumiun  12040  isumlessdc  12059  expcnv  12067  prodmodc  12141  zproddc  12142  iprodap  12143  iprodap0  12145  fprodssdc  12153  prodsnf  12155  fprodsplitdc  12159  fprodsplit  12160  fprodm1  12161  fprod1p  12162  fprodunsn  12167  fprod2dlemstep  12185  fprodsplitsn  12196  ef0lem  12223  modmulconst  12386  dvdsdivcl  12413  dvdsssfz1  12415  dvdsfac  12423  zeoxor  12432  nn0ehalf  12466  nn0oddm1d2  12472  nnoddm1d2  12473  divalglemeunn  12484  divalglemeuneg  12486  bitsfzolem  12517  bitsinv1  12525  gcdsupex  12530  gcdsupcl  12531  bezoutlemnewy  12569  bezoutlemmain  12571  bezoutlemeu  12580  dfgcd2  12587  nnwosdc  12612  nninfct  12614  algrf  12619  algcvgblem  12623  lcmgcdlem  12651  lcmdvds  12653  coprmgcdb  12662  mulgcddvds  12668  qredeu  12671  cncongr1  12677  cncongr2  12678  isprm2lem  12690  dvdsnprmd  12699  prmdc  12704  oddprmge3  12709  pw2dvdseu  12742  phibndlem  12790  dfphi2  12794  hashdvds  12795  phiprmpw  12796  eulerthlemh  12805  hashgcdeq  12814  phisum  12815  odzdvds  12820  reumodprminv  12828  nnnn0modprm0  12830  prm23ge5  12839  pclemdc  12863  pcdvdsb  12895  difsqpwdvds  12913  oddprmdvds  12929  1arith  12942  4sqlem3  12965  4sqlemafi  12970  4sqlemffi  12971  4sqleminfi  12972  4sqexercise1  12973  4sqlem11  12976  4sqlem19  12984  ennnfonelemdc  13022  ennnfonelemh  13027  ennnfonelemhf1o  13036  ennnfonelemf1  13041  ennnfonelemrn  13042  ennnfonelemdm  13043  exmidunben  13049  ctinfomlemom  13050  ctinfom  13051  ctiunctlemudc  13060  ctiunctlemf  13061  ctiunctal  13064  nninfdclemcl  13071  nninfdclemf  13072  nninfdclemp1  13073  isstructim  13098  setsresg  13122  strleund  13188  1strbas  13202  2strbasg  13205  2stropg  13206  restsspw  13334  tgval  13347  ptex  13349  imasaddfnlemg  13399  fnpr2o  13424  fnpr2ob  13425  mgmidsssn0  13469  fngsum  13473  igsumvalx  13474  isnsgrp  13491  sgrpidmndm  13505  mndinvmod  13530  mnd1  13540  mhmeql  13577  grpinveu  13623  prdsinvlem  13693  mulgval  13711  subgintm  13787  trivsubgsnd  13790  eqgfval  13811  ecqusaddd  13827  ecqusaddcl  13828  ghmeql  13856  iscmnd  13887  imasabl  13925  gsumfzmhm2  13933  rnglz  13961  srgfcl  13989  rhmopp  14193  subrgdvds  14252  lssuni  14380  lssintclm  14401  lspf  14406  qusmulrng  14549  mulgrhm2  14627  znf1o  14668  psrbagfi  14690  psr1clfi  14705  mplsubgfilemcl  14716  istopon  14740  toponcom  14754  topgele  14756  topontopn  14764  tsettps  14765  eltg2b  14781  unitg  14789  tgss2  14806  bastop2  14811  distop  14812  epttop  14817  cldss2  14833  neisspw  14875  neipsm  14881  neiuni  14888  tgcn  14935  tgcnp  14936  cnntr  14952  lmff  14976  txuni2  14983  txbasex  14984  txbas  14985  txcnp  14998  txcnmpt  15000  txcn  15002  txdis  15004  txdis1cn  15005  cnmpt11  15010  cnmpt12  15014  cnmpt21  15018  cnmpt2t  15020  cnmpt22  15021  blsscls2  15220  xmetxpbl  15235  xmettxlem  15236  tgqioo  15282  fsumcncntop  15294  cncfmpt1f  15325  mulcncflem  15334  mulcncf  15335  dedekindeu  15350  dedekindicclemicc  15359  dedekindicc  15360  ivthinclemdisj  15367  hovercncf  15373  limcimo  15392  cnmptlimc  15401  reldvg  15406  dvfvalap  15408  dvfgg  15415  dvmptfsum  15452  dveflem  15453  dvef  15454  elply2  15462  sincn  15496  coscn  15497  reeff1o  15500  pilem3  15510  ioocosf1o  15581  mpodvdsmulf1o  15717  fsumdvdsmul  15718  perfectlem2  15727  lgsne0  15770  gausslemma2dlem1a  15790  gausslemma2dlem4  15796  lgseisenlem2  15803  lgseisenlem3  15804  lgsquadlem2  15810  2lgslem3  15833  2sqlem2  15847  mul2sq  15848  2sqlem3  15849  2sqlem7  15853  edgstruct  15918  pw0ss  15937  incistruhgr  15944  upgrex  15957  umgrnloop0  15971  upgr1een  15978  lfgrnloopen  15987  umgredg  15999  umgrnloop2  16005  uspgredgiedg  16032  uspgriedgedg  16033  usgrislfuspgrdom  16044  usgredg3  16068  uspgredg2vlem  16074  uspgredg2v  16075  ushgredgedg  16080  ushgredgedgloop  16082  uhgr0vsize0en  16089  usgr1e  16095  subusgr  16129  vtxedgfi  16143  vtxlpfi  16144  vtxdumgrfival  16152  1loopgrvd2fi  16159  p1evtxdeqfilem  16165  vdegp1aid  16168  wlkcprim  16204  wlk1walkdom  16213  uspgr2wlkeq  16219  upgr2wlkdc  16231  wlkres  16233  clwwlkccatlem  16254  clwwlknp  16271  umgr2cwwk2dif  16278  trlsegvdegfi  16321  eupth2lem3lem3fi  16324  eupth2lem3lem6fi  16325  eupth2lem3lem4fi  16327  eupth2lembfi  16331  depindlem1  16346  bj-trst  16356  bj-fast  16358  bj-stand  16365  bj-trdc  16369  bj-fadc  16371  decidr  16413  djulclALT  16418  djurclALT  16419  bj-charfunr  16426  bj-indind  16548  bj-2inf  16554  bj-nntrans2  16568  bj-peano4  16571  bj-nnord  16574  bj-inf2vn  16590  bj-inf2vn2  16591  bj-findis  16595  pwf1oexmid  16621  subctctexmid  16622  pw1dceq  16626  nnsf  16628  nninfsellemdc  16633  nninffeq  16643  nnnninfen  16644  exmidsbthrlem  16647  sbthom  16651  triap  16654  trilpo  16668  apdifflemr  16672  redcwlpo  16680  tridceq  16681  nconstwlpolem0  16688  nconstwlpolem  16690  nconstwlpo  16691  neapmkv  16693  ltlenmkv  16695  gfsump1  16707