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  3brtr4g  4164  trin  4239  triun  4242  truni  4243  trint  4244  iinexgm  4290  class2seteq  4300  pwuni  4329  exmid1dc  4337  exmidn0m  4338  exmidsssn  4339  exmid0el  4341  exmidel  4342  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  mss  4366  copsex2t  4385  euotd  4395  pwunim  4431  ispod  4449  sotricim  4468  exse  4481  frind  4497  trssord  4525  suctr  4566  pwnex  4595  eusvnf  4599  eusvnfb  4600  eusv2nf  4602  rexxfrd  4609  ralxfr2d  4610  rexxfr2d  4611  rabxfrd  4615  reuhypd  4617  eldifpw  4623  iunpw  4626  ssorduni  4634  onsucb  4650  onsucelsucr  4655  sucunielr  4657  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmid  4677  reg2exmidlema  4681  setindel  4685  elirr  4688  orddisj  4693  en2lp  4701  suc11g  4704  ordsuc  4710  nlimsucg  4713  ordtri2or2exmid  4718  ontri2orexmidim  4719  zfregfr  4721  wessep  4725  tfi  4729  peano5  4745  limom  4761  peano2b  4762  nndceq0  4765  nnpredcl  4770  0nelrel  4821  eqrelrdv  4871  xpsspw  4887  relint  4901  relop  4930  eqbrrdva  4950  ssrelrn  4972  opeldm  4984  reldmm  5000  elres  5099  relssres  5101  elrelimasn  5153  exse2  5161  issref  5170  trin2  5179  dminss  5202  imainss  5203  rnxpid  5222  dmsn0el  5257  dmmptg  5285  relrelss  5314  cnviinm  5329  iotanul  5353  sniota  5368  dffun5r  5389  funmo  5392  funco  5417  funun  5422  fununmo  5423  fununfun  5424  funprg  5431  funtpg  5432  funtp  5434  fntpg  5437  fununi  5449  funcnvuni  5450  imadiflem  5460  imainlem  5462  funimaexglem  5464  isarep2  5468  fnunsn  5490  2elresin  5494  fnimadisj  5504  dmmptd  5514  fco  5552  funssxp  5557  fssres  5565  feu  5574  fimacnvdisj  5576  fabexg  5579  f00  5584  f0rn0  5587  f1co  5610  fores  5625  foco  5626  f1ores  5654  foimacnv  5657  f1oun  5659  fun11iun  5660  f1oco  5662  fo00  5677  brprcneu  5688  fv3  5718  relelfvdm  5727  nfvres  5732  nfunsn  5733  funfvbrb  5822  respreima  5836  dff2  5852  dff3im  5853  dffo4  5856  fvmptelcdm  5861  ffvresb  5871  f1oresrab  5873  fmptco  5874  fsn  5880  fcof  5894  fpr  5897  ftpg  5899  fsnunf  5915  fsnunfv  5916  elabrex  5963  dff1o6  5982  foeqcnvco  5996  fliftel1  6000  isores1  6020  isoini2  6025  riotasbc  6055  acexmidlemph  6078  acexmidlemcase  6080  oprabidlem  6116  brabvv  6134  eloprabga  6175  fnoprabg  6189  caovimo  6283  oprabexd  6360  uchoice  6371  fo1stresm  6395  fo2ndresm  6396  unielxp  6408  1st2ndbr  6418  opabn1stprc  6429  fmpoco  6452  1stconst  6457  2ndconst  6458  poxp  6468  spc2ed  6469  disjxp1  6472  elmpom  6474  suppsnopdc  6490  reldmtpos  6524  tposfun  6531  dftpos4  6534  smores  6563  smores2  6565  tfrlem1  6579  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemibex  6600  tfrlemiubacc  6601  tfrlemi14d  6604  tfrexlem  6605  tfri1d  6606  tfr1onlembxssdm  6614  tfr1onlembex  6616  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllembxssdm  6627  tfrcllembex  6629  tfrcllemubacc  6630  tfrcllemres  6633  tfri3  6638  rdgon  6657  frecabcl  6670  frecfcllem  6675  frecrdg  6679  2oconcl  6712  nnsucelsuc  6764  nntri3or  6766  nndceq  6772  nndcel  6773  dcdifsnid  6777  ecexr  6812  brdifun  6834  ecelqsdm  6879  iinerm  6881  eroveu  6900  erovlem  6901  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  fsetdmprc0  6950  pmsspw  6964  map0b  6968  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpf  7002  uniixp  7003  ixpexgg  7004  resixp  7015  f1oen3g  7040  ssdomg  7065  domtr  7072  snfig  7103  modom  7108  enpr2d  7111  dom1o  7116  xpf1o  7144  xpmapenlem  7149  php5dom  7164  fidceq  7171  nnfi  7174  fiunsnnn  7185  findcard  7192  findcard2  7193  findcard2s  7194  ac6sfi  7202  fidcen  7203  tridc  7204  fimax2gtri  7206  finexdc  7207  elssdc  7209  eqsndc  7210  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  tpfidisj  7236  tpfidceq  7237  exmidssfi  7246  iunfidisj  7260  mapfi  7261  fissfi  7263  snexxph  7267  fidcenumlemrks  7270  sbthlem2  7275  sbthlemi3  7276  sbthlem7  7280  sbthlemi8  7281  fival  7304  dcfi  7315  fdcf1  7316  f1setfi  7317  supmoti  7334  djuss  7411  updjudhf  7420  updjud  7423  casefun  7426  caseinj  7430  omp1eomlem  7435  djufun  7445  djuinj  7447  ctssdccl  7452  ctfoex  7459  nnnninf  7467  nnnninfeq2  7470  nninfisollem0  7471  nninfisollemne  7472  nninfisollemeq  7473  nninfisol  7474  finomni  7481  exmidomniim  7482  exmidomni  7483  fodjuomnilemdc  7485  omniwomnimkv  7508  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemg  7516  nninfwlpoim  7520  nninfinfwlpo  7521  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  finacn  7561  exmidaclem  7565  dju1en  7570  exmidontriimlem1  7578  exmidontriimlem3  7580  iftrueb01  7583  pw1on  7586  3nsssucpw1  7596  2omotaplemap  7624  2omotap  7626  exmidmotap  7628  cc4f  7636  cc4n  7638  acnccim  7639  dmaddpqlem  7745  nqpi  7746  dmaddpq  7747  dmmulpq  7748  ltdcnq  7765  subhalfnqq  7782  enq0sym  7800  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  nq0nn  7810  addnq0mo  7815  mulnq0mo  7816  nqpnq0nq  7821  nqnq0a  7822  nqnq0m  7823  npsspw  7839  elnp1st2nd  7844  prnmaxl  7856  prnminu  7857  prarloc  7871  genprndl  7889  genprndu  7890  nqprm  7910  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  prmuloc  7934  mulnqprlemrl  7941  mulnqprlemru  7942  ltsopr  7964  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  lteupri  7985  recexprlemopl  7993  recexprlemopu  7995  recexprlemdisj  7998  archpr  8011  cauappcvgprlemdisj  8019  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  caucvgprlemnbj  8035  caucvgprlemdisj  8042  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemnbj  8061  caucvgprprlemdisj  8070  suplocexprlemml  8084  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemloc  8089  addsrmo  8111  mulsrmo  8112  recexgt0sr  8141  prsrpos  8153  caucvgsrlemasr  8158  suplocsrlemb  8174  suplocsrlempr  8175  suplocsr  8177  elrealeu  8197  pitonn  8216  pitoregt0  8217  pitore  8218  recnnre  8219  axaddcl  8232  axaddrcl  8233  axmulcl  8234  axmulrcl  8235  axrnegex  8247  axcnre  8249  axpre-lttrn  8252  rereceu  8257  axarch  8259  axpre-suploclemres  8269  axpre-suploc  8270  ltxrlt  8392  apirr  8936  divmulasscomap  9029  rerecclap  9063  lbreu  9278  indconst1  9306  arch  9565  0mnnnnn0  9600  nnm1nn0  9609  elnnnn0c  9613  elnnz1  9672  ztri3or0  9691  nzadd  9702  nn0n0n1ge2  9720  zdceq  9725  zdcle  9726  zdclt  9727  uzind  9762  eluzge3nn  9982  supinfneg  10005  infsupneg  10006  eluz2b2  10013  elnn1uz2  10017  elnn0dc  10021  elnndc  10022  nn01to3  10027  znq  10034  qaddcl  10045  qmulcl  10047  qreccl  10052  irradd  10056  irrmul  10058  elpq  10060  cnref1o  10062  xnn0dcle  10215  xrpnfdc  10255  xrmnfdc  10256  xaddcom  10274  xnegdi  10281  xpncan  10284  xleadd1a  10286  iooidg  10322  elioo4g  10347  elfzd  10430  fzdcel  10455  fznlem  10456  fzpreddisj  10489  fz0to4untppr  10542  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  4fvwrd4  10558  fzosplit  10597  elfzo0  10604  nn0p1elfzo  10605  fzo1fzo0n0  10606  elfzonn0  10609  fzofzim  10611  elfzo1  10614  elfzom1elp1fzo  10631  fzossfzop1  10641  ssfzo12bi  10654  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  qdceq  10690  qdclt  10691  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnxr  10703  modfzo0difsn  10846  frec2uzrand  10856  frec2uzf1od  10857  frecuzrdgrcl  10861  frecuzrdgtcl  10863  frecuzrdgrclt  10866  frecuzrdgfunlem  10870  frecfzennn  10877  nninfinf  10894  seq3f1olemp  10966  seq3f1oleml  10967  seqf1oglem1  10970  ser0f  10985  expcl2lemap  11002  hashunsng  11263  hashmap  11283  sshashneg  11296  hashfibclem  11297  hashfibc  11298  hashf1lem1  11300  hashf1lem2  11301  iswrdinn0  11324  snopiswrd  11329  wrdlndm  11336  iswrdsymb  11337  wrdsymb1  11356  ccatfv0  11386  ccatval21sw  11388  lswccatn0lsw  11394  eqs1  11411  ccat1st1st  11424  lswccats1fst  11427  fzowrddc  11434  swrdfv0  11441  swrdlen2  11449  swrdfv2  11450  swrdsbslen  11453  swrdspsleq  11454  pfxfv0  11479  pfxtrcfv0  11481  pfxeq  11483  pfx1  11490  swrdswrdlem  11491  cats1un  11508  pfxccatin12lem2a  11514  pfxccatin12lem2  11518  pfxccatin12lem3  11519  swrdccat  11522  cats1fvn  11551  cats1fvnd  11552  shftfvalg  11598  shftfval  11601  caucvgre  11762  rexanuz  11769  recvguniq  11776  rennim  11783  resqrexlemf  11788  rsqrmo  11808  fimaxre2  12009  climeu  12080  sumdc  12142  summodc  12168  zsumdc  12169  isum  12170  fisumss  12177  isumss2  12178  fsumsplit  12192  sumsnf  12194  fsumsplitsn  12195  sumtp  12199  sumsplitdc  12217  fsum2dlemstep  12219  fisum0diag2  12232  fsumconst  12239  modfsummodlemstep  12242  fsum00  12247  fsumabs  12250  fsumiun  12262  isumlessdc  12281  expcnv  12289  prodmodc  12363  zproddc  12364  iprodap  12365  iprodap0  12367  fprodssdc  12375  prodsnf  12377  fprodsplitdc  12381  fprodsplit  12382  fprodm1  12383  fprod1p  12384  fprodunsn  12389  fprod2dlemstep  12407  fprodsplitsn  12418  ef0lem  12445  modmulconst  12608  dvdsdivcl  12635  dvdsssfz1  12637  dvdsfac  12645  zeoxor  12654  nn0ehalf  12688  nn0oddm1d2  12694  nnoddm1d2  12695  divalglemeunn  12706  divalglemeuneg  12708  bitsfzolem  12739  bitsinv1  12747  gcdsupex  12752  gcdsupcl  12753  bezoutlemnewy  12791  bezoutlemmain  12793  bezoutlemeu  12802  dfgcd2  12809  nnwosdc  12834  nninfct  12836  algrf  12841  algcvgblem  12845  lcmgcdlem  12873  lcmdvds  12875  coprmgcdb  12884  mulgcddvds  12890  qredeu  12893  cncongr1  12899  cncongr2  12900  isprm2lem  12912  dvdsnprmd  12921  prmdc  12926  prmdcz  12927  oddprmge3  12932  pwbdvdseu  12965  nn0sqdcq  13006  phibndlem  13016  dfphi2  13020  hashdvds  13021  phiprmpw  13022  eulerthlemh  13031  hashgcdeq  13040  phisum  13041  odzdvds  13046  reumodprminv  13054  nnnn0modprm0  13056  prm23ge5  13065  pclemdc  13089  pcdvdsb  13121  difsqpwdvds  13139  oddprmdvds  13155  1arith  13168  4sqlem3  13191  4sqlemafi  13196  4sqlemffi  13197  4sqleminfi  13198  4sqexercise1  13199  4sqlem11  13202  4sqlem19  13210  ballotfilemcdc  13274  ballotfilemdifcfi  13276  ballotfilemdifcfz  13278  ballotfilem2  13279  ballotfilemiex  13295  ballotfilemscl  13298  ballotfilemth  13332  ennnfonelemdc  13341  ennnfonelemh  13346  ennnfonelemhf1o  13355  ennnfonelemf1  13360  ennnfonelemrn  13361  ennnfonelemdm  13362  exmidunben  13368  ctinfomlemom  13369  ctinfom  13370  ctiunctlemudc  13379  ctiunctlemf  13380  ctiunctal  13383  nninfdclemcl  13390  nninfdclemf  13391  nninfdclemp1  13392  isstructim  13417  setsresg  13441  strleund  13508  1strbas  13522  2strbasg  13525  2stropg  13526  restsspw  13654  tgval  13667  ptex  13669  imasaddfnlemg  13686  fnpr2o  13711  fnpr2ob  13712  mgmidsssn0  13755  fngzsum  13759  gzsumvalx  13760  isnsgrp  13772  sgrpidmndm  13784  mndinvmod  13809  mnd1  13813  mhmeql  13850  grpinveu  13894  mulgval  13976  subgintm  14052  trivsubgsnd  14055  eqgfval  14076  ecqusaddd  14092  ecqusaddcl  14093  ghmeql  14121  iscmnd  14152  imasabl  14191  gzsummhm2  14197  gsump1  14208  gsummhm2fi  14216  prdsinvlem  14247  rnglz  14295  srgfcl  14328  rhmopp  14534  opprlring  14555  subrgdvds  14594  lssuni  14751  lssintclm  14772  lspf  14777  qusmulrng  14920  mulgrhm2  14996  znf1o  15037  aspid  15068  psrbagfi  15110  psrbagconcl  15115  psr1clfi  15131  mplsubgfilemcl  15142  istopon  15166  toponcom  15180  topgele  15182  topontopn  15190  tsettps  15191  eltg2b  15207  unitg  15215  tgss2  15232  bastop2  15237  distop  15238  epttop  15243  cldss2  15259  neisspw  15301  neipsm  15307  neiuni  15314  tgcn  15361  tgcnp  15362  cnntr  15378  lmff  15402  txuni2  15409  txbasex  15410  txbas  15411  txcnp  15424  txcnmpt  15426  txcn  15428  txdis  15430  txdis1cn  15431  cnmpt11  15436  cnmpt12  15440  cnmpt21  15444  cnmpt2t  15446  cnmpt22  15447  blsscls2  15646  xmetxpbl  15661  xmettxlem  15662  tgqioo  15708  fsumcncntop  15720  cncfmpt1f  15751  mulcncflem  15760  mulcncf  15761  dedekindeu  15776  dedekindicclemicc  15785  dedekindicc  15786  ivthinclemdisj  15793  hovercncf  15799  limcimo  15818  cnmptlimc  15827  reldvg  15832  dvfvalap  15834  dvfgg  15841  dvmptfsum  15878  dveflem  15879  dvef  15880  elply2  15888  sincn  15922  coscn  15923  reeff1o  15926  pilem3  15937  ioocosf1o  16008  ppiqfi  16164  prmdvdsfi  16165  ppiprm  16181  ppinprm  16182  chtprm  16183  chtnprm  16184  chtdif  16186  efchtqdvds  16187  ppidif  16191  prmorcht  16204  mpodvdsmulf1o  16206  fsumdvdsmul  16207  ppiqub  16215  perfectlem2  16222  bcmono  16226  lgsne0  16279  gausslemma2dlem1a  16299  gausslemma2dlem4  16305  lgseisenlem2  16312  lgseisenlem3  16313  lgsquadlem2  16319  2lgslem3  16342  2sqlem2  16356  mul2sq  16357  2sqlem3  16358  2sqlem7  16362  edgstruct  16427  pw0ss  16446  incistruhgr  16453  upgrex  16466  umgrnloop0  16480  upgr1een  16487  lfgrnloopen  16496  umgredg  16508  umgrnloop2  16514  uspgredgiedg  16541  uspgriedgedg  16542  usgrislfuspgrdom  16553  usgredg3  16577  uspgredg2vlem  16583  uspgredg2v  16584  ushgredgedg  16589  ushgredgedgloop  16591  uhgr0vsize0en  16598  usgr1e  16604  subusgr  16638  vtxedgfi  16652  vtxlpfi  16653  vtxdumgrfival  16661  1loopgrvd2fi  16668  p1evtxdeqfilem  16674  vdegp1aid  16677  wlkcprim  16713  wlk1walkdom  16722  uspgr2wlkeq  16728  upgr2wlkdc  16740  wlkres  16742  clwwlkccatlem  16763  clwwlknp  16780  umgr2cwwk2dif  16787  trlsegvdegfi  16830  eupth2lem3lem3fi  16833  eupth2lem3lem6fi  16834  eupth2lem3lem4fi  16836  eupth2lembfi  16840  depindlem1  16869  bj-trst  16889  bj-fast  16891  bj-stand  16898  bj-trdc  16902  bj-fadc  16904  decidr  16946  djulclALT  16951  djurclALT  16952  bj-charfunr  16958  bj-indind  17080  bj-2inf  17086  bj-nntrans2  17100  bj-peano4  17103  bj-nnord  17106  bj-inf2vn  17122  bj-inf2vn2  17123  bj-findis  17127  pwf1oexmid  17151  subctctexmid  17152  pw1dceq  17157  exmidnotnotr  17158  exmidcon  17159  exmidpeirce  17160  wexmiddc  17164  wexmiddiffi  17166  wexmiddifxylem  17167  wexmiddifxy  17168  nnsf  17170  nninfsellemdc  17175  nninffeq  17185  nnnninfen  17186  exmidsbthrlem  17189  sbthom  17193  triap  17200  trilpo  17214  apdifflemr  17218  redcwlpo  17227  tridceq  17228  nconstwlpolem0  17235  nconstwlpolem  17237  nconstwlpo  17238  neapmkv  17240  ltlenmkv  17242