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  414  oibabs  704  dcim  831  dcstab  834  stdcndc  835  stdcndcOLD  836  dcor  925  3mix1  1156  3mix2  1157  3jca  1167  syl3anbrc  1171  syl21anbrc  1172  inegd  1362  pclem6  1364  xoranor  1367  nfxfrd  1463  nfd  1511  hban  1535  nfan1  1552  nford  1555  nfand  1556  hbim1  1558  nfal  1564  alexim  1633  nnal  1637  ax6blem  1638  nf4r  1659  19.34  1672  nfexd  1749  sbcof2  1798  nfsb2or  1825  sbidm  1839  nfdv  1865  nfd2  2010  nfeudv  2029  mon  2043  eumo  2046  mo23  2055  eu2  2058  eu3h  2059  exmodc  2064  exmonim  2065  mo2r  2066  mo3h  2067  bm1.1  2150  eqrdv  2163  3eltr4g  2251  abbi2dv  2284  abbi1dv  2285  nfcd  2302  nfcxfrd  2305  dcned  2341  neqned  2342  3netr4g  2370  necon3bi  2385  necon2ai  2389  nnral  2455  alral  2510  rspe  2514  rsp2e  2516  rgen2a  2519  ralrimi  2536  r19.27v  2592  r19.28v  2593  r19.27av  2600  r19.32r  2611  nfreudxy  2638  mormo  2676  nrexrmo  2681  cgsex2g  2761  cgsex4g  2762  spc2egv  2815  spc2gv  2816  spc3egv  2817  spc3gv  2818  rspce  2824  ceqex  2852  elrab3t  2880  elrabd  2883  mosubt  2902  mo2icl  2904  reu3  2915  reu6i  2916  2rmorex  2931  sbc5  2973  rspesbca  3034  rmo2ilem  3039  sbnfc2  3104  ssrd  3146  ssrdv  3147  3sstr4g  3184  eqsstrid  3187  ss2abdv  3214  abssdv  3215  rabssdv  3221  ss2rabdv  3222  ssun1  3284  unssad  3298  unssbd  3299  ssddif  3355  uneqin  3372  indifdir  3377  undif3ss  3382  reuss2  3401  n0rf  3420  reximdva0m  3423  rabxmdc  3439  ssindif0im  3467  minel  3469  ralidm  3508  ralm  3512  dcun  3518  ifmdc  3557  disjsn2  3638  absneu  3647  rabsneu  3648  opprc  3778  elunii  3793  dfnfc2  3806  uniss2  3819  unidif  3820  ssunieq  3821  intab  3852  iunss2  3910  iunxdif2  3913  invdisj  3975  disjiun  3976  3brtr4g  4015  trin  4089  triun  4092  truni  4093  trint  4094  iinexgm  4132  class2seteq  4141  pwuni  4170  exmid1dc  4178  exmidn0m  4179  exmidsssn  4180  exmid0el  4182  exmidel  4183  exmidundif  4184  exmidundifim  4185  mss  4203  copsex2t  4222  euotd  4231  pwunim  4263  ispod  4281  sotricim  4300  exse  4313  frind  4329  trssord  4357  suctr  4398  pwnex  4426  eusvnf  4430  eusvnfb  4431  eusv2nf  4433  rexxfrd  4440  ralxfr2d  4441  rexxfr2d  4442  rabxfrd  4446  reuhypd  4448  eldifpw  4454  iunpw  4457  ssorduni  4463  sucelon  4479  onsucelsucr  4484  sucunielr  4486  ontriexmidim  4498  ordtri2or2exmidlem  4502  onsucelsucexmid  4506  reg2exmidlema  4510  setindel  4514  elirr  4517  orddisj  4522  en2lp  4530  suc11g  4533  ordsuc  4539  nlimsucg  4542  ordtri2or2exmid  4547  ontri2orexmidim  4548  zfregfr  4550  wessep  4554  tfi  4558  peano5  4574  limom  4590  peano2b  4591  nndceq0  4594  nnpredcl  4599  0nelrel  4649  eqrelrdv  4699  xpsspw  4715  relint  4727  relop  4753  eqbrrdva  4773  opeldm  4806  elres  4919  relssres  4921  exse2  4977  issref  4985  trin2  4994  dminss  5017  imainss  5018  rnxpid  5037  dmsn0el  5072  dmmptg  5100  relrelss  5129  cnviinm  5144  iotanul  5167  sniota  5179  dffun5r  5199  funmo  5202  funco  5227  funun  5231  funprg  5237  funtpg  5238  funtp  5240  fntpg  5243  fununi  5255  funcnvuni  5256  imadiflem  5266  imainlem  5268  funimaexglem  5270  isarep2  5274  fnunsn  5294  2elresin  5298  fnimadisj  5307  dmmptd  5317  fco  5352  funssxp  5356  fssres  5362  feu  5369  fimacnvdisj  5371  fabexg  5374  f00  5378  f0rn0  5381  f1co  5404  fores  5418  foco  5419  f1ores  5446  foimacnv  5449  f1oun  5451  fun11iun  5452  f1oco  5454  fo00  5467  brprcneu  5478  fv3  5508  relelfvdm  5517  nfvres  5518  nfunsn  5519  funfvbrb  5597  respreima  5612  dff2  5628  dff3im  5629  dffo4  5632  fvmptelrn  5637  ffvresb  5647  f1oresrab  5649  fmptco  5650  fsn  5656  fpr  5666  ftpg  5668  fsnunf  5684  fsnunfv  5685  elabrex  5725  dff1o6  5743  foeqcnvco  5757  fliftel1  5761  isores1  5781  isoini2  5786  riotasbc  5812  acexmidlemph  5834  acexmidlemcase  5836  oprabidlem  5869  brabvv  5884  eloprabga  5925  fnoprabg  5939  caovimo  6031  oprabexd  6092  fo1stresm  6126  fo2ndresm  6127  unielxp  6139  1st2ndbr  6149  fmpoco  6180  1stconst  6185  2ndconst  6186  poxp  6196  spc2ed  6197  disjxp1  6200  reldmtpos  6217  tposfun  6224  dftpos4  6227  smores  6256  smores2  6258  tfrlem1  6272  tfr0dm  6286  tfrlemibxssdm  6291  tfrlemibex  6293  tfrlemiubacc  6294  tfrlemi14d  6297  tfrexlem  6298  tfri1d  6299  tfr1onlembxssdm  6307  tfr1onlembex  6309  tfr1onlemubacc  6310  tfr1onlemres  6313  tfrcllemsucfn  6317  tfrcllembxssdm  6320  tfrcllembex  6322  tfrcllemubacc  6323  tfrcllemres  6326  tfri3  6331  rdgon  6350  frecabcl  6363  frecfcllem  6368  frecrdg  6372  2oconcl  6403  nnsucelsuc  6455  nntri3or  6457  nndceq  6463  nndcel  6464  dcdifsnid  6468  ecexr  6502  brdifun  6524  ecelqsdm  6567  iinerm  6569  eroveu  6588  erovlem  6589  ecopovtrn  6594  ecopovtrng  6597  th3qlem1  6599  pmsspw  6645  map0b  6649  mapsn  6652  mapsncnv  6657  ixpf  6682  uniixp  6683  ixpexgg  6684  resixp  6695  f1oen3g  6716  ssdomg  6740  domtr  6747  snfig  6776  enpr2d  6779  xpf1o  6806  xpmapenlem  6811  php5dom  6825  fidceq  6831  nnfi  6834  fiunsnnn  6843  findcard  6850  findcard2  6851  findcard2s  6852  ac6sfi  6860  tridc  6861  fimax2gtri  6863  finexdc  6864  exmidpw  6870  exmidpweq  6871  nnwetri  6877  unsnfi  6880  unsnfidcex  6881  unsnfidcel  6882  undifdcss  6884  tpfidisj  6889  iunfidisj  6907  snexxph  6911  fidcenumlemrks  6914  sbthlem2  6919  sbthlemi3  6920  sbthlem7  6924  sbthlemi8  6925  fival  6931  dcfi  6942  supmoti  6954  djuss  7031  updjudhf  7040  updjud  7043  casefun  7046  caseinj  7050  omp1eomlem  7055  djufun  7065  djuinj  7067  ctssdccl  7072  ctfoex  7079  nnnninf  7086  nnnninfeq2  7089  nninfisollem0  7090  nninfisollemne  7091  nninfisollemeq  7092  nninfisol  7093  finomni  7100  exmidomniim  7101  exmidomni  7102  fodjuomnilemdc  7104  omniwomnimkv  7127  exmidonfinlem  7145  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  dju1en  7165  exmidontriimlem1  7173  exmidontriimlem3  7175  pw1on  7178  3nsssucpw1  7188  cc4f  7206  cc4n  7208  dmaddpqlem  7314  nqpi  7315  dmaddpq  7316  dmmulpq  7317  ltdcnq  7334  subhalfnqq  7351  enq0sym  7369  enq0ref  7370  enq0tr  7371  nqnq0pi  7375  nq0nn  7379  addnq0mo  7384  mulnq0mo  7385  nqpnq0nq  7390  nqnq0a  7391  nqnq0m  7392  npsspw  7408  elnp1st2nd  7413  prnmaxl  7425  prnminu  7426  prarloc  7440  genprndl  7458  genprndu  7459  nqprm  7479  nqprl  7488  nqpru  7489  addnqprlemrl  7494  addnqprlemru  7495  prmuloc  7503  mulnqprlemrl  7510  mulnqprlemru  7511  ltsopr  7533  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemopu  7540  lteupri  7554  recexprlemopl  7562  recexprlemopu  7564  recexprlemdisj  7567  archpr  7580  cauappcvgprlemdisj  7588  cauappcvgprlemladdrl  7594  cauappcvgprlem2  7597  caucvgprlemnbj  7604  caucvgprlemdisj  7611  caucvgprlemladdfu  7614  caucvgprlem2  7617  caucvgprprlemnbj  7630  caucvgprprlemdisj  7639  suplocexprlemml  7653  suplocexprlemrl  7654  suplocexprlemmu  7655  suplocexprlemloc  7658  addsrmo  7680  mulsrmo  7681  recexgt0sr  7710  prsrpos  7722  caucvgsrlemasr  7727  suplocsrlemb  7743  suplocsrlempr  7744  suplocsr  7746  elrealeu  7766  pitonn  7785  pitoregt0  7786  pitore  7787  recnnre  7788  axaddcl  7801  axaddrcl  7802  axmulcl  7803  axmulrcl  7804  axrnegex  7816  axcnre  7818  axpre-lttrn  7821  rereceu  7826  axarch  7828  axpre-suploclemres  7838  axpre-suploc  7839  ltxrlt  7960  apirr  8499  divmulasscomap  8588  rerecclap  8622  lbreu  8836  arch  9107  0mnnnnn0  9142  nnm1nn0  9151  elnnnn0c  9155  elnnz1  9210  ztri3or0  9229  nzadd  9239  nn0n0n1ge2  9257  zdceq  9262  zdcle  9263  zdclt  9264  uzind  9298  eluzge3nn  9506  supinfneg  9529  infsupneg  9530  eluz2b2  9537  elnn1uz2  9541  elnn0dc  9545  elnndc  9546  nn01to3  9551  znq  9558  qaddcl  9569  qmulcl  9571  qreccl  9576  irradd  9580  irrmul  9581  elpq  9582  cnref1o  9584  xnn0dcle  9734  xrpnfdc  9774  xrmnfdc  9775  xaddcom  9793  xnegdi  9800  xpncan  9803  xleadd1a  9805  iooidg  9841  elioo4g  9866  fzdcel  9971  fznlem  9972  fzpreddisj  10002  fz0to4untppr  10055  elfz0ubfz0  10056  elfz0fzfz0  10057  fz0fzelfz0  10058  fz0fzdiffz0  10061  elfzmlbp  10063  difelfzle  10065  4fvwrd4  10071  fzosplit  10108  elfzo0  10113  fzo1fzo0n0  10114  elfzonn0  10117  fzofzim  10119  elfzo1  10121  elfzom1elp1fzo  10133  fzossfzop1  10143  ssfzo12bi  10156  exfzdc  10171  qdceq  10178  exbtwnzlemstep  10179  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2z  10186  qbtwnxr  10189  modfzo0difsn  10326  frec2uzrand  10336  frec2uzf1od  10337  frecuzrdgrcl  10341  frecuzrdgtcl  10343  frecuzrdgrclt  10346  frecuzrdgfunlem  10350  frecfzennn  10357  seq3f1olemp  10433  seq3f1oleml  10434  ser0f  10446  expcl2lemap  10463  hashunsng  10716  shftfvalg  10756  shftfval  10759  caucvgre  10919  rexanuz  10926  recvguniq  10933  rennim  10940  resqrexlemf  10945  rsqrmo  10965  fimaxre2  11164  climeu  11233  sumdc  11295  summodc  11320  zsumdc  11321  isum  11322  fisumss  11329  isumss2  11330  fsumsplit  11344  sumsnf  11346  fsumsplitsn  11347  sumtp  11351  sumsplitdc  11369  fsum2dlemstep  11371  fisum0diag2  11384  fsumconst  11391  modfsummodlemstep  11394  fsum00  11399  fsumabs  11402  fsumiun  11414  isumlessdc  11433  expcnv  11441  prodmodc  11515  zproddc  11516  iprodap  11517  iprodap0  11519  fprodssdc  11527  prodsnf  11529  fprodsplitdc  11533  fprodsplit  11534  fprodm1  11535  fprod1p  11536  fprodunsn  11541  fprod2dlemstep  11559  fprodsplitsn  11570  ef0lem  11597  modmulconst  11759  dvdsdivcl  11784  dvdsssfz1  11786  dvdsfac  11794  zeoxor  11802  nn0ehalf  11836  nn0oddm1d2  11842  nnoddm1d2  11843  divalglemeunn  11854  divalglemeuneg  11856  zsupcllemstep  11874  infssuzex  11878  gcdsupex  11886  gcdsupcl  11887  bezoutlemnewy  11925  bezoutlemmain  11927  bezoutlemeu  11936  dfgcd2  11943  nnwosdc  11968  algrf  11973  algcvgblem  11977  lcmgcdlem  12005  lcmdvds  12007  coprmgcdb  12016  mulgcddvds  12022  qredeu  12025  cncongr1  12031  cncongr2  12032  isprm2lem  12044  dvdsnprmd  12053  prmdc  12058  oddprmge3  12063  pw2dvdseu  12096  phibndlem  12144  dfphi2  12148  hashdvds  12149  phiprmpw  12150  eulerthlemh  12159  hashgcdeq  12167  phisum  12168  odzdvds  12173  reumodprminv  12181  nnnn0modprm0  12183  prm23ge5  12192  pclemdc  12216  pcdvdsb  12247  difsqpwdvds  12265  oddprmdvds  12280  1arith  12293  4sqlem3  12316  ennnfonelemdc  12328  ennnfonelemh  12333  ennnfonelemhf1o  12342  ennnfonelemf1  12347  ennnfonelemrn  12348  ennnfonelemdm  12349  exmidunben  12355  ctinfomlemom  12356  ctinfom  12357  ctiunctlemudc  12366  ctiunctlemf  12367  ctiunctal  12370  nninfdclemcl  12377  nninfdclemf  12378  nninfdclemp1  12379  isstructim  12404  setsresg  12428  strleund  12478  1strbas  12489  2strbasg  12491  2stropg  12492  restsspw  12561  istopon  12611  toponcom  12625  topgele  12627  topontopn  12635  tsettps  12636  tgval  12649  eltg2b  12654  unitg  12662  tgss2  12679  bastop2  12684  distop  12685  epttop  12690  cldss2  12706  neisspw  12748  neipsm  12754  neiuni  12761  tgcn  12808  tgcnp  12809  cnntr  12825  lmff  12849  txuni2  12856  txbasex  12857  txbas  12858  txcnp  12871  txcnmpt  12873  txcn  12875  txdis  12877  txdis1cn  12878  cnmpt11  12883  cnmpt12  12887  cnmpt21  12891  cnmpt2t  12893  cnmpt22  12894  blsscls2  13093  xmetxpbl  13108  xmettxlem  13109  tgqioo  13147  fsumcncntop  13156  cncfmpt1f  13184  mulcncflem  13190  mulcncf  13191  dedekindeu  13201  dedekindicclemicc  13210  dedekindicc  13211  ivthinclemdisj  13218  limcimo  13234  cnmptlimc  13243  reldvg  13248  dvfvalap  13250  dvfgg  13257  dveflem  13287  dvef  13288  sincn  13290  coscn  13291  reeff1o  13294  pilem3  13304  ioocosf1o  13375  lgsne0  13539  2sqlem2  13551  mul2sq  13552  2sqlem3  13553  2sqlem7  13557  bj-trst  13580  bj-fast  13582  bj-stand  13589  bj-trdc  13593  bj-fadc  13595  decidr  13637  djulclALT  13642  djurclALT  13643  bj-charfunr  13652  bj-indind  13774  bj-2inf  13780  bj-nntrans2  13794  bj-peano4  13797  bj-nnord  13800  bj-inf2vn  13816  bj-inf2vn2  13817  bj-findis  13821  pwf1oexmid  13839  exmid1stab  13840  subctctexmid  13841  nnsf  13845  nninfsellemdc  13850  nninffeq  13860  exmidsbthrlem  13861  sbthom  13865  triap  13868  trilpo  13882  apdifflemr  13886  redcwlpo  13894  tridceq  13895  nconstwlpolem0  13901  nconstwlpolem  13903  nconstwlpo  13904  neapmkv  13906