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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbbr  136  pm5.74rd  183  bitri  184  3imtr4i  201  sylanbrc  421  mpnanrd  704  oibabs  726  dcim  853  dcstab  856  stdcndc  857  stdcndcOLD  858  dcand  945  dcor  948  dfifp2dc  994  3mix1  1197  3mix2  1198  3jca  1208  syl3anbrc  1212  syl21anbrc  1213  inegd  1421  pclem6  1423  xoranor  1426  dcfrompeirce  1499  nfxfrd  1528  nfd  1576  hban  1600  nfan1  1617  nford  1620  nfand  1621  hbim1  1623  nfal  1629  alexim  1698  nnal  1702  hbn  1703  nf4r  1723  19.34  1736  nfexd  1814  sbcof2  1863  nfsb2or  1890  sbidm  1904  nfdv  1930  nfd2  2082  nfeudv  2101  mon  2115  eumo  2118  mo23  2128  eu2  2131  eu3h  2132  exmodc  2137  exmonim  2138  mo2r  2139  mo3h  2140  bm1.1  2223  eqrdv  2236  3eltr4g  2324  abbi2dv  2359  abbi1dv  2360  nfcd  2387  nfcxfrd  2390  dcned  2426  neqned  2427  3netr4g  2455  necon3bi  2470  necon2ai  2474  nnral  2540  alral  2595  rspe  2599  rsp2e  2601  rgen2a  2604  ralrimi  2621  r19.27v  2678  r19.28v  2679  r19.27av  2686  r19.32r  2697  nfreudxy  2725  mormo  2769  nrexrmo  2774  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  rspce  2924  ceqex  2953  elrab3t  2981  elrabd  2984  mosubt  3003  mo2icl  3005  reu3  3016  reu6i  3017  2rmorex  3032  sbc5  3075  rspesbca  3137  rmo2ilem  3142  sbnfc2  3208  ssrd  3253  ssrdv  3254  3sstr4g  3291  eqsstrid  3294  ss2abdv  3321  abssdv  3322  rabssdv  3328  ss2rabdv  3329  ssun1  3392  unssad  3406  unssbd  3407  ssddif  3465  uneqin  3482  indifdir  3487  undif3ss  3492  reuss2  3513  n0rf  3534  reximdva0m  3537  rabxmdc  3554  ssindif0im  3584  minel  3586  ralidm  3628  ralm  3631  dcun  3637  ifmdc  3683  ifeqeqxdc  3687  disjsn2  3772  rabsnif  3778  absneu  3783  rabsneu  3784  opprc  3925  elunii  3940  dfnfc2  3953  uniss2  3966  unidif  3967  ssunieq  3968  intab  3999  iunss2  4057  iunssd  4058  iunxdif2  4061  invdisj  4123  disjiun  4125  sn0disj  4127  3brtr4g  4165  trin  4241  triun  4244  truni  4245  trint  4246  iinexgm  4292  class2seteq  4302  pwuni  4331  exmid1dc  4339  exmidn0m  4340  exmidsssn  4341  exmid0el  4343  exmidel  4344  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  mss  4368  copsex2t  4387  euotd  4397  pwunim  4433  ispod  4451  sotricim  4470  exse  4483  frind  4499  trssord  4527  suctr  4568  pwnex  4597  eusvnf  4601  eusvnfb  4602  eusv2nf  4604  rexxfrd  4611  ralxfr2d  4612  rexxfr2d  4613  rabxfrd  4617  reuhypd  4619  eldifpw  4625  iunpw  4628  ssorduni  4636  onsucb  4652  onsucelsucr  4657  sucunielr  4659  ontriexmidim  4671  ordtri2or2exmidlem  4675  onsucelsucexmid  4679  reg2exmidlema  4683  setindel  4687  elirr  4690  orddisj  4695  en2lp  4703  suc11g  4706  ordsuc  4712  nlimsucg  4715  ordtri2or2exmid  4720  ontri2orexmidim  4721  zfregfr  4723  wessep  4727  tfi  4731  peano5  4747  limom  4763  peano2b  4764  nndceq0  4767  nnpredcl  4772  0nelrel  4823  eqrelrdv  4873  xpsspw  4889  relint  4903  relop  4932  eqbrrdva  4952  ssrelrn  4974  opeldm  4986  reldmm  5002  elres  5101  relssres  5103  elrelimasn  5156  exse2  5164  issref  5173  trin2  5182  dminss  5205  imainss  5206  rnxpid  5225  dmsn0el  5260  dmmptg  5288  relrelss  5317  cnviinm  5332  iotanul  5356  sniota  5371  dffun5r  5392  funmo  5395  funco  5420  funun  5425  fununmo  5426  fununfun  5427  funprg  5434  funtpg  5435  funtp  5437  fntpg  5440  fununi  5452  funcnvuni  5453  imadiflem  5463  imainlem  5465  funimaexglem  5467  isarep2  5471  fnunsn  5493  2elresin  5497  fnimadisj  5507  dmmptd  5517  fco  5555  funssxp  5560  fssres  5568  feu  5577  fimacnvdisj  5579  fabexg  5582  f00  5587  f0rn0  5590  f1co  5613  fores  5628  foco  5629  f1ores  5657  foimacnv  5660  f1oun  5662  fun11iun  5663  f1oco  5665  fo00  5680  brprcneu  5691  fv3  5721  relelfvdm  5730  nfvres  5735  nfunsn  5736  funfvbrb  5825  respreima  5839  dff2  5855  dff3im  5856  dffo4  5859  fvmptelcdm  5864  ffvresb  5874  f1oresrab  5876  fmptco  5877  fsn  5883  fcof  5897  fpr  5900  ftpg  5902  fsnunf  5918  fsnunfv  5919  elabrex  5966  dff1o6  5985  foeqcnvco  5999  fliftel1  6003  isores1  6023  isoini2  6028  riotasbc  6058  acexmidlemph  6081  acexmidlemcase  6083  oprabidlem  6119  brabvv  6137  eloprabga  6178  fnoprabg  6192  caovimo  6286  oprabexd  6364  uchoice  6375  fo1stresm  6399  fo2ndresm  6400  unielxp  6412  1st2ndbr  6422  opabn1stprc  6433  fmpoco  6456  1stconst  6461  2ndconst  6462  poxp  6472  spc2ed  6473  disjxp1  6476  elmpom  6478  suppsnopdc  6494  reldmtpos  6529  tposfun  6536  dftpos4  6539  smores  6568  smores2  6570  tfrlem1  6584  tfr0dm  6598  tfrlemibxssdm  6603  tfrlemibex  6605  tfrlemiubacc  6606  tfrlemi14d  6609  tfrexlem  6610  tfri1d  6611  tfr1onlembxssdm  6619  tfr1onlembex  6621  tfr1onlemubacc  6622  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllembxssdm  6632  tfrcllembex  6634  tfrcllemubacc  6635  tfrcllemres  6638  tfri3  6643  rdgon  6662  frecabcl  6675  frecfcllem  6680  frecrdg  6684  2oconcl  6717  nnsucelsuc  6769  nntri3or  6771  nndceq  6777  nndcel  6778  dcdifsnid  6782  ecexr  6817  brdifun  6839  ecelqsdm  6884  iinerm  6886  eroveu  6905  erovlem  6906  ecopovtrn  6911  ecopovtrng  6914  th3qlem1  6916  fsetdmprc0  6955  pmsspw  6969  map0b  6973  mapsnd  6976  mapsn  6978  mapsncnv  6983  ixpf  7008  uniixp  7009  ixpexgg  7010  resixp  7021  f1oen3g  7046  ssdomg  7071  domtr  7078  snfig  7109  modom  7114  enpr2d  7117  dom1o  7122  xpf1o  7150  xpmapenlem  7155  php5dom  7170  fidceq  7177  nnfi  7180  fiunsnnn  7191  findcard  7198  findcard2  7199  findcard2s  7200  ac6sfi  7208  fidcen  7209  tridc  7210  fimax2gtri  7212  finexdc  7213  elssdc  7215  eqsndc  7216  exmidpw  7221  exmidpweq  7222  exmidpw2en  7225  nnwetri  7229  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  tpfidisj  7242  tpfidceq  7243  exmidssfi  7252  iunfidisj  7266  mapfi  7267  fissfi  7269  snexxph  7274  fidcenumlemrks  7277  sbthlem2  7282  sbthlemi3  7283  sbthlem7  7287  sbthlemi8  7288  fival  7309  dcfi  7320  fdcf1  7321  f1setfi  7322  supmoti  7339  djuss  7416  updjudhf  7425  updjud  7428  casefun  7431  caseinj  7435  omp1eomlem  7440  djufun  7450  djuinj  7452  ctssdccl  7457  ctfoex  7464  nnnninf  7472  nnnninfeq2  7475  nninfisollem0  7476  nninfisollemne  7477  nninfisollemeq  7478  nninfisol  7479  finomni  7486  exmidomniim  7487  exmidomni  7488  fodjuomnilemdc  7490  omniwomnimkv  7513  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoim  7525  nninfinfwlpo  7526  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  finacn  7566  exmidaclem  7570  dju1en  7575  exmidontriimlem1  7583  exmidontriimlem3  7585  iftrueb01  7588  pw1on  7591  3nsssucpw1  7601  2omotaplemap  7629  2omotap  7631  exmidmotap  7633  cc4f  7641  cc4n  7643  acnccim  7644  dmaddpqlem  7750  nqpi  7751  dmaddpq  7752  dmmulpq  7753  ltdcnq  7770  subhalfnqq  7787  enq0sym  7805  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  nq0nn  7815  addnq0mo  7820  mulnq0mo  7821  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  npsspw  7844  elnp1st2nd  7849  prnmaxl  7861  prnminu  7862  prarloc  7876  genprndl  7894  genprndu  7895  nqprm  7915  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  prmuloc  7939  mulnqprlemrl  7946  mulnqprlemru  7947  ltsopr  7969  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  lteupri  7990  recexprlemopl  7998  recexprlemopu  8000  recexprlemdisj  8003  archpr  8016  cauappcvgprlemdisj  8024  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemnbj  8040  caucvgprlemdisj  8047  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemnbj  8066  caucvgprprlemdisj  8075  suplocexprlemml  8089  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemloc  8094  addsrmo  8116  mulsrmo  8117  recexgt0sr  8146  prsrpos  8158  caucvgsrlemasr  8163  suplocsrlemb  8179  suplocsrlempr  8180  suplocsr  8182  elrealeu  8202  pitonn  8221  pitoregt0  8222  pitore  8223  recnnre  8224  axaddcl  8237  axaddrcl  8238  axmulcl  8239  axmulrcl  8240  axrnegex  8252  axcnre  8254  axpre-lttrn  8257  rereceu  8262  axarch  8264  axpre-suploclemres  8274  axpre-suploc  8275  ltxrlt  8397  apirr  8941  divmulasscomap  9034  rerecclap  9068  lbreu  9283  indconst1  9312  arch  9571  0mnnnnn0  9606  nnm1nn0  9615  elnnnn0c  9619  elnnz1  9676  ztri3or0  9695  nzadd  9706  nn0n0n1ge2  9724  zdceq  9729  zdcle  9730  zdclt  9731  uzind  9767  eluzge3nn  9987  supinfneg  10010  infsupneg  10011  eluz2b2  10018  elnn1uz2  10022  elnn0dc  10026  elnndc  10027  nn01to3  10032  znq  10039  qaddcl  10050  qmulcl  10052  qreccl  10057  irradd  10061  irrmul  10063  elpq  10065  cnref1o  10067  xnn0dcle  10220  xrpnfdc  10260  xrmnfdc  10261  xaddcom  10279  xnegdi  10286  xpncan  10289  xleadd1a  10291  iooidg  10327  elioo4g  10352  elfzd  10435  fzdcel  10460  fznlem  10461  fzpreddisj  10494  fz0to4untppr  10547  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  elfzmlbp  10555  difelfzle  10557  4fvwrd4  10563  fzosplit  10602  elfzo0  10609  nn0p1elfzo  10610  fzo1fzo0n0  10611  elfzonn0  10614  fzofzim  10616  elfzo1  10619  elfzom1elp1fzo  10636  fzossfzop1  10646  ssfzo12bi  10659  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  qdceq  10695  qdclt  10696  exbtwnzlemstep  10698  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnxr  10708  modfzo0difsn  10852  frec2uzrand  10862  frec2uzf1od  10863  frecuzrdgrcl  10867  frecuzrdgtcl  10869  frecuzrdgrclt  10872  frecuzrdgfunlem  10876  frecfzennn  10883  nninfinf  10900  seq3f1olemp  10972  seq3f1oleml  10973  seqf1oglem1  10976  ser0f  10991  expcl2lemap  11008  hashunsng  11269  hashmap  11289  sshashneg  11302  hashfibclem  11303  hashfibc  11304  hashf1lem1  11306  hashf1lem2  11307  iswrdinn0  11330  snopiswrd  11335  wrdlndm  11342  iswrdsymb  11343  wrdsymb1  11362  ccatfv0  11392  ccatval21sw  11394  lswccatn0lsw  11400  eqs1  11417  ccat1st1st  11430  lswccats1fst  11433  fzowrddc  11440  swrdfv0  11447  swrdlen2  11455  swrdfv2  11456  swrdsbslen  11459  swrdspsleq  11460  pfxfv0  11485  pfxtrcfv0  11487  pfxeq  11489  pfx1  11496  swrdswrdlem  11497  cats1un  11514  pfxccatin12lem2a  11520  pfxccatin12lem2  11524  pfxccatin12lem3  11525  swrdccat  11528  cats1fvn  11557  cats1fvnd  11558  shftfvalg  11604  shftfval  11607  caucvgre  11768  rexanuz  11775  recvguniq  11782  rennim  11789  resqrexlemf  11794  rsqrmo  11814  fimaxre2  12015  climeu  12086  sumdc  12148  summodc  12174  zsumdc  12175  isum  12176  fisumss  12183  isumss2  12184  fsumsplit  12198  sumsnf  12200  fsumsplitsn  12201  sumtp  12205  sumsplitdc  12223  fsum2dlemstep  12225  fisum0diag2  12238  fsumconst  12245  modfsummodlemstep  12248  fsum00  12253  fsumabs  12256  fsumiun  12268  isumlessdc  12287  expcnv  12295  prodmodc  12369  zproddc  12370  iprodap  12371  iprodap0  12373  fprodssdc  12381  prodsnf  12383  fprodsplitdc  12387  fprodsplit  12388  fprodm1  12389  fprod1p  12390  fprodunsn  12395  fprod2dlemstep  12413  fprodsplitsn  12424  ef0lem  12451  modmulconst  12614  dvdsdivcl  12641  dvdsssfz1  12643  dvdsfac  12651  zeoxor  12660  nn0ehalf  12694  nn0oddm1d2  12700  nnoddm1d2  12701  divalglemeunn  12712  divalglemeuneg  12714  bitsfzolem  12745  bitsinv1  12753  gcdsupex  12758  gcdsupcl  12759  bezoutlemnewy  12797  bezoutlemmain  12799  bezoutlemeu  12808  dfgcd2  12815  nnwosdc  12840  nninfct  12842  algrf  12847  algcvgblem  12851  lcmgcdlem  12879  lcmdvds  12881  coprmgcdb  12890  mulgcddvds  12896  qredeu  12899  cncongr1  12905  cncongr2  12906  isprm2lem  12918  dvdsnprmd  12927  prmdc  12932  prmdcz  12933  oddprmge3  12938  pwbdvdseu  12971  nn0sqdcq  13012  phibndlem  13022  dfphi2  13026  hashdvds  13027  phiprmpw  13028  eulerthlemh  13037  hashgcdeq  13046  phisum  13047  odzdvds  13052  reumodprminv  13060  nnnn0modprm0  13062  prm23ge5  13071  pclemdc  13095  pcdvdsb  13127  difsqpwdvds  13145  oddprmdvds  13161  1arith  13174  4sqlem3  13197  4sqlemafi  13202  4sqlemffi  13203  4sqleminfi  13204  4sqexercise1  13205  4sqlem11  13208  4sqlem19  13216  ballotfilemcdc  13280  ballotfilemdifcfi  13282  ballotfilemdifcfz  13284  ballotfilem2  13285  ballotfilemiex  13301  ballotfilemscl  13304  ballotfilemth  13338  ennnfonelemdc  13347  ennnfonelemh  13352  ennnfonelemhf1o  13361  ennnfonelemf1  13366  ennnfonelemrn  13367  ennnfonelemdm  13368  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  ctiunctlemudc  13385  ctiunctlemf  13386  ctiunctal  13389  nninfdclemcl  13396  nninfdclemf  13397  nninfdclemp1  13398  isstructim  13423  setsresg  13447  strleund  13515  1strbas  13529  2strbasg  13532  2stropg  13533  restsspw  13661  tgval  13674  ptex  13676  imasaddfnlemg  13693  fnpr2o  13718  fnpr2ob  13719  mgmidsssn0  13762  fngzsum  13766  gzsumvalx  13767  isnsgrp  13779  sgrpidmndm  13791  mndinvmod  13816  mnd1  13820  mhmeql  13857  grpinveu  13901  mulgval  13983  subgintm  14059  trivsubgsnd  14062  eqgfval  14083  ecqusaddd  14099  ecqusaddcl  14100  ghmeql  14128  iscmnd  14190  imasabl  14229  gzsummhm2  14235  gsump1  14246  gsummptfidmsplit  14253  gsumsnfdcmn  14256  gsumunsnfd  14258  gsummhm2fi  14264  gsum2dfilem2  14271  gsumcom2fi  14274  prdsinvlem  14302  rnglz  14350  srgfcl  14383  rhmopp  14591  opprlring  14612  subrgdvds  14651  lssuni  14808  lssintclm  14829  lspf  14834  qusmulrng  14977  mulgrhm2  15053  znf1o  15094  aspid  15125  psrbagfi  15166  psrbagconcl  15176  psr1clfi  15207  mvrclfi  15226  istopon  15256  toponcom  15270  topgele  15272  topontopn  15280  tsettps  15281  eltg2b  15297  unitg  15305  tgss2  15322  bastop2  15327  distop  15328  epttop  15333  cldss2  15349  neisspw  15391  neipsm  15397  neiuni  15404  tgcn  15451  tgcnp  15452  cnntr  15468  lmff  15492  txuni2  15499  txbasex  15500  txbas  15501  txcnp  15514  txcnmpt  15516  txcn  15518  txdis  15520  txdis1cn  15521  cnmpt11  15526  cnmpt12  15530  cnmpt21  15534  cnmpt2t  15536  cnmpt22  15537  blsscls2  15736  xmetxpbl  15751  xmettxlem  15752  tgqioo  15798  fsumcncntop  15810  cncfmpt1f  15841  mulcncflem  15850  mulcncf  15851  dedekindeu  15866  dedekindicclemicc  15875  dedekindicc  15876  ivthinclemdisj  15883  hovercncf  15889  limcimo  15908  cnmptlimc  15917  reldvg  15922  dvfvalap  15924  dvfgg  15931  dvmptfsum  15968  dveflem  15969  dvef  15970  elply2  15978  sincn  16012  coscn  16013  reeff1o  16016  pilem3  16027  ioocosf1o  16099  ppiqfi  16259  prmdvdsfi  16260  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  chtdif  16281  efchtqdvds  16282  ppidif  16286  prmorcht  16299  mpodvdsmulf1o  16301  fsumdvdsmul  16302  ppiqub  16310  perfectlem2  16317  bcmono  16321  bpos  16337  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem2  16419  2lgslem3  16442  2sqlem2  16456  mul2sq  16457  2sqlem3  16458  2sqlem7  16462  edgstruct  16527  pw0ss  16546  incistruhgr  16553  upgrex  16566  umgrnloop0  16580  upgr1een  16587  lfgrnloopen  16596  umgredg  16608  umgrnloop2  16614  uspgredgiedg  16641  uspgriedgedg  16642  usgrislfuspgrdom  16653  usgredg3  16677  uspgredg2vlem  16683  uspgredg2v  16684  ushgredgedg  16689  ushgredgedgloop  16691  uhgr0vsize0en  16698  usgr1e  16704  subusgr  16738  vtxedgfi  16752  vtxlpfi  16753  vtxdumgrfival  16761  1loopgrvd2fi  16768  p1evtxdeqfilem  16774  vdegp1aid  16777  wlkcprim  16813  wlk1walkdom  16822  uspgr2wlkeq  16828  upgr2wlkdc  16840  wlkres  16842  clwwlkccatlem  16863  clwwlknp  16880  umgr2cwwk2dif  16887  trlsegvdegfi  16930  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  eupth2lembfi  16940  depindlem1  16969  bj-trst  16989  bj-fast  16991  bj-stand  16998  bj-trdc  17002  bj-fadc  17004  decidr  17046  djulclALT  17051  djurclALT  17052  bj-charfunr  17058  bj-indind  17180  bj-2inf  17186  bj-nntrans2  17200  bj-peano4  17203  bj-nnord  17206  bj-inf2vn  17222  bj-inf2vn2  17223  bj-findis  17227  pwf1oexmid  17251  subctctexmid  17252  pw1dceq  17257  exmidnotnotr  17258  exmidcon  17259  exmidpeirce  17260  wexmiddc  17264  wexmiddiffi  17266  wexmiddifxylem  17267  wexmiddifxy  17268  nnsf  17271  nninfsellemdc  17276  nninffeq  17286  nnnninfen  17287  exmidsbthrlem  17290  sbthom  17294  triap  17301  trilpo  17316  apdifflemr  17320  redcwlpo  17329  tridceq  17330  nconstwlpolem0  17337  nconstwlpolem  17339  nconstwlpo  17340  neapmkv  17342  ltlenmkv  17344