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	|- ( ph -> ps )
sylibr.2	|- ( ch <-> ps )

Assertion

Ref	Expression
sylibr	|- ( ph -> ch )

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 |- ( ph -> ps )
2		sylibr.2	. . 3 |- ( ch <-> ps )
3	2	biimpri 132	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

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  2012  mon  2026  eumo  2029  mo23  2038  eu2  2041  eu3h  2042  exmodc  2047  exmonim  2048  mo2r  2049  mo3h  2050  bm1.1  2122  eqrdv  2135  3eltr4g  2223  abbi2dv  2256  abbi1dv  2257  nfcd  2274  nfcxfrd  2277  dcned  2312  neqned  2313  3netr4g  2341  necon3bi  2356  necon2ai  2360  alral  2476  rspe  2479  rsp2e  2481  rgen2a  2484  ralrimi  2501  r19.27v  2557  r19.28v  2558  r19.27av  2565  r19.32r  2576  nfreudxy  2602  mormo  2640  nrexrmo  2645  cgsex2g  2717  cgsex4g  2718  spc2egv  2770  spc2gv  2771  spc3egv  2772  spc3gv  2773  rspce  2779  ceqex  2807  elrab3t  2834  elrabd  2837  mosubt  2856  mo2icl  2858  reu3  2869  reu6i  2870  2rmorex  2885  sbc5  2927  rspesbca  2988  rmo2ilem  2993  sbnfc2  3055  ssrd  3097  ssrdv  3098  3sstr4g  3135  eqsstrid  3138  ss2abdv  3165  abssdv  3166  rabssdv  3172  ss2rabdv  3173  ssun1  3234  unssad  3248  unssbd  3249  ssddif  3305  uneqin  3322  indifdir  3327  undif3ss  3332  reuss2  3351  n0rf  3370  reximdva0m  3373  rabxmdc  3389  ssindif0im  3417  minel  3419  ralidm  3458  ralm  3462  dcun  3468  ifmdc  3504  disjsn2  3581  absneu  3590  rabsneu  3591  opprc  3721  elunii  3736  dfnfc2  3749  uniss2  3762  unidif  3763  ssunieq  3764  intab  3795  iunss2  3853  iunxdif2  3856  invdisj  3918  disjiun  3919  3brtr4g  3957  trin  4031  triun  4034  truni  4035  trint  4036  iinexgm  4074  class2seteq  4082  pwuni  4111  exmid1dc  4118  exmidn0m  4119  exmidsssn  4120  exmid0el  4122  exmidel  4123  exmidundif  4124  exmidundifim  4125  mss  4143  copsex2t  4162  euotd  4171  pwunim  4203  ispod  4221  sotricim  4240  exse  4253  frind  4269  trssord  4297  suctr  4338  pwnex  4365  eusvnf  4369  eusvnfb  4370  eusv2nf  4372  rexxfrd  4379  ralxfr2d  4380  rexxfr2d  4381  rabxfrd  4385  reuhypd  4387  eldifpw  4393  iunpw  4396  ssorduni  4398  sucelon  4414  onsucelsucr  4419  sucunielr  4421  ordtri2or2exmidlem  4436  onsucelsucexmid  4440  reg2exmidlema  4444  setindel  4448  elirr  4451  orddisj  4456  en2lp  4464  suc11g  4467  ordsuc  4473  nlimsucg  4476  ordtri2or2exmid  4481  zfregfr  4483  wessep  4487  tfi  4491  peano5  4507  limom  4522  peano2b  4523  nndceq0  4526  nnpredcl  4531  0nelrel  4580  eqrelrdv  4630  xpsspw  4646  relint  4658  relop  4684  eqbrrdva  4704  opeldm  4737  elres  4850  relssres  4852  exse2  4908  issref  4916  trin2  4925  dminss  4948  imainss  4949  rnxpid  4968  dmsn0el  5003  dmmptg  5031  relrelss  5060  cnviinm  5075  iotanul  5098  sniota  5110  dffun5r  5130  funmo  5133  funco  5158  funun  5162  funprg  5168  funtpg  5169  funtp  5171  fntpg  5174  fununi  5186  funcnvuni  5187  imadiflem  5197  imainlem  5199  funimaexglem  5201  isarep2  5205  fnunsn  5225  2elresin  5229  fnimadisj  5238  dmmptd  5248  fco  5283  funssxp  5287  fssres  5293  feu  5300  fimacnvdisj  5302  fabexg  5305  f00  5309  f0rn0  5312  f1co  5335  fores  5349  foco  5350  f1ores  5375  foimacnv  5378  f1oun  5380  fun11iun  5381  f1oco  5383  fo00  5396  brprcneu  5407  fv3  5437  relelfvdm  5446  nfvres  5447  nfunsn  5448  funfvbrb  5526  respreima  5541  dff2  5557  dff3im  5558  dffo4  5561  fvmptelrn  5566  ffvresb  5576  f1oresrab  5578  fmptco  5579  fsn  5585  fpr  5595  ftpg  5597  fsnunf  5613  fsnunfv  5614  elabrex  5652  dff1o6  5670  foeqcnvco  5684  fliftel1  5688  isores1  5708  isoini2  5713  riotasbc  5738  acexmidlemph  5760  acexmidlemcase  5762  oprabidlem  5795  brabvv  5810  eloprabga  5851  fnoprabg  5865  caovimo  5957  oprabexd  6018  fo1stresm  6052  fo2ndresm  6053  unielxp  6065  1st2ndbr  6075  fmpoco  6106  1stconst  6111  2ndconst  6112  poxp  6122  spc2ed  6123  disjxp1  6126  reldmtpos  6143  tposfun  6150  dftpos4  6153  smores  6182  smores2  6184  tfrlem1  6198  tfr0dm  6212  tfrlemibxssdm  6217  tfrlemibex  6219  tfrlemiubacc  6220  tfrlemi14d  6223  tfrexlem  6224  tfri1d  6225  tfr1onlembxssdm  6233  tfr1onlembex  6235  tfr1onlemubacc  6236  tfr1onlemres  6239  tfrcllemsucfn  6243  tfrcllembxssdm  6246  tfrcllembex  6248  tfrcllemubacc  6249  tfrcllemres  6252  tfri3  6257  rdgon  6276  frecabcl  6289  frecfcllem  6294  frecrdg  6298  2oconcl  6329  nnsucelsuc  6380  nntri3or  6382  nndceq  6388  nndcel  6389  dcdifsnid  6393  ecexr  6427  brdifun  6449  ecelqsdm  6492  iinerm  6494  eroveu  6513  erovlem  6514  ecopovtrn  6519  ecopovtrng  6522  th3qlem1  6524  pmsspw  6570  map0b  6574  mapsn  6577  mapsncnv  6582  ixpf  6607  uniixp  6608  ixpexgg  6609  resixp  6620  f1oen3g  6641  ssdomg  6665  domtr  6672  snfig  6701  enpr2d  6704  xpf1o  6731  xpmapenlem  6736  php5dom  6750  fidceq  6756  nnfi  6759  fiunsnnn  6768  findcard  6775  findcard2  6776  findcard2s  6777  ac6sfi  6785  tridc  6786  fimax2gtri  6788  finexdc  6789  exmidpw  6795  nnwetri  6797  unsnfi  6800  unsnfidcex  6801  unsnfidcel  6802  undifdcss  6804  tpfidisj  6809  iunfidisj  6827  snexxph  6831  fidcenumlemrks  6834  sbthlem2  6839  sbthlemi3  6840  sbthlem7  6844  sbthlemi8  6845  fival  6851  supmoti  6873  djuss  6948  updjudhf  6957  updjud  6960  casefun  6963  caseinj  6967  omp1eomlem  6972  djufun  6982  djuinj  6984  ctssdccl  6989  ctfoex  6996  finomni  7005  exmidomniim  7006  exmidomni  7007  fodjuomnilemdc  7009  nnnninf  7016  exmidonfinlem  7042  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  dju1en  7062  dmaddpqlem  7178  nqpi  7179  dmaddpq  7180  dmmulpq  7181  ltdcnq  7198  subhalfnqq  7215  enq0sym  7233  enq0ref  7234  enq0tr  7235  nqnq0pi  7239  nq0nn  7243  addnq0mo  7248  mulnq0mo  7249  nqpnq0nq  7254  nqnq0a  7255  nqnq0m  7256  npsspw  7272  elnp1st2nd  7277  prnmaxl  7289  prnminu  7290  prarloc  7304  genprndl  7322  genprndu  7323  nqprm  7343  nqprl  7352  nqpru  7353  addnqprlemrl  7358  addnqprlemru  7359  prmuloc  7367  mulnqprlemrl  7374  mulnqprlemru  7375  ltsopr  7397  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemopu  7404  lteupri  7418  recexprlemopl  7426  recexprlemopu  7428  recexprlemdisj  7431  archpr  7444  cauappcvgprlemdisj  7452  cauappcvgprlemladdrl  7458  cauappcvgprlem2  7461  caucvgprlemnbj  7468  caucvgprlemdisj  7475  caucvgprlemladdfu  7478  caucvgprlem2  7481  caucvgprprlemnbj  7494  caucvgprprlemdisj  7503  suplocexprlemml  7517  suplocexprlemrl  7518  suplocexprlemmu  7519  suplocexprlemloc  7522  addsrmo  7544  mulsrmo  7545  recexgt0sr  7574  prsrpos  7586  caucvgsrlemasr  7591  suplocsrlemb  7607  suplocsrlempr  7608  suplocsr  7610  elrealeu  7630  pitonn  7649  pitoregt0  7650  pitore  7651  recnnre  7652  axaddcl  7665  axaddrcl  7666  axmulcl  7667  axmulrcl  7668  axrnegex  7680  axcnre  7682  axpre-lttrn  7685  rereceu  7690  axarch  7692  axpre-suploclemres  7702  axpre-suploc  7703  ltxrlt  7823  apirr  8360  cnstab  8400  divmulasscomap  8449  rerecclap  8483  lbreu  8696  arch  8967  0mnnnnn0  9002  nnm1nn0  9011  elnnnn0c  9015  elnnz1  9070  ztri3or0  9089  nzadd  9099  nn0n0n1ge2  9114  zdceq  9119  zdcle  9120  zdclt  9121  uzind  9155  eluzge3nn  9360  supinfneg  9383  infsupneg  9384  eluz2b2  9390  elnn1uz2  9394  nn01to3  9402  znq  9409  qaddcl  9420  qmulcl  9422  qreccl  9427  irradd  9431  irrmul  9432  cnref1o  9433  xrpnfdc  9618  xrmnfdc  9619  xaddcom  9637  xnegdi  9644  xpncan  9647  xleadd1a  9649  iooidg  9685  elioo4g  9710  fzdcel  9813  fznlem  9814  fzpreddisj  9844  elfz0ubfz0  9895  elfz0fzfz0  9896  fz0fzelfz0  9897  fz0fzdiffz0  9900  elfzmlbp  9902  difelfzle  9904  4fvwrd4  9910  fzosplit  9947  elfzo0  9952  fzo1fzo0n0  9953  elfzonn0  9956  fzofzim  9958  elfzo1  9960  elfzom1elp1fzo  9972  fzossfzop1  9982  ssfzo12bi  9995  exfzdc  10010  qdceq  10017  exbtwnzlemstep  10018  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  qbtwnxr  10028  modfzo0difsn  10161  frec2uzrand  10171  frec2uzf1od  10172  frecuzrdgrcl  10176  frecuzrdgtcl  10178  frecuzrdgrclt  10181  frecuzrdgfunlem  10185  frecfzennn  10192  seq3f1olemp  10268  seq3f1oleml  10269  ser0f  10281  expcl2lemap  10298  hashunsng  10546  shftfvalg  10583  shftfval  10586  caucvgre  10746  rexanuz  10753  recvguniq  10760  rennim  10767  resqrexlemf  10772  rsqrmo  10792  fimaxre2  10991  climeu  11058  sumdc  11120  summodc  11145  zsumdc  11146  isum  11147  fisumss  11154  isumss2  11155  fsumsplit  11169  sumsnf  11171  fsumsplitsn  11172  sumtp  11176  sumsplitdc  11194  fsum2dlemstep  11196  fisum0diag2  11209  fsumconst  11216  modfsummodlemstep  11219  fsum00  11224  fsumabs  11227  fsumiun  11239  isumlessdc  11258  expcnv  11266  ef0lem  11355  modmulconst  11514  dvdsdivcl  11537  dvdsssfz1  11539  dvdsfac  11547  zeoxor  11555  nn0ehalf  11589  nn0oddm1d2  11595  nnoddm1d2  11596  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemstep  11627  infssuzex  11631  gcdsupex  11635  gcdsupcl  11636  bezoutlemnewy  11673  bezoutlemmain  11675  bezoutlemeu  11684  dfgcd2  11691  algrf  11715  algcvgblem  11719  lcmgcdlem  11747  lcmdvds  11749  coprmgcdb  11758  mulgcddvds  11764  qredeu  11767  cncongr1  11773  cncongr2  11774  isprm2lem  11786  dvdsnprmd  11795  oddprmge3  11804  pw2dvdseu  11835  phibndlem  11881  dfphi2  11885  hashdvds  11886  phiprmpw  11887  hashgcdeq  11893  ennnfonelemdc  11901  ennnfonelemh  11906  ennnfonelemhf1o  11915  ennnfonelemf1  11920  ennnfonelemrn  11921  ennnfonelemdm  11922  exmidunben  11928  ctinfomlemom  11929  ctinfom  11930  ctiunctlemudc  11939  ctiunctlemf  11940  isstructim  11962  setsresg  11986  strleund  12036  1strbas  12047  2strbasg  12049  2stropg  12050  restsspw  12119  istopon  12169  toponcom  12183  topgele  12185  topontopn  12193  tsettps  12194  tgval  12207  eltg2b  12212  unitg  12220  tgss2  12237  bastop2  12242  distop  12243  epttop  12248  cldss2  12264  neisspw  12306  neipsm  12312  neiuni  12319  tgcn  12366  tgcnp  12367  cnntr  12383  lmff  12407  txuni2  12414  txbasex  12415  txbas  12416  txcnp  12429  txcnmpt  12431  txcn  12433  txdis  12435  txdis1cn  12436  cnmpt11  12441  cnmpt12  12445  cnmpt21  12449  cnmpt2t  12451  cnmpt22  12452  blsscls2  12651  xmetxpbl  12666  xmettxlem  12667  tgqioo  12705  fsumcncntop  12714  cncfmpt1f  12742  mulcncflem  12748  mulcncf  12749  dedekindeu  12759  dedekindicclemicc  12768  dedekindicc  12769  ivthinclemdisj  12776  limcimo  12792  cnmptlimc  12801  reldvg  12806  dvfvalap  12808  dvfgg  12815  dveflem  12844  dvef  12845  sincn  12847  coscn  12848  pilem3  12853  bj-nnal  12938  bj-trst  12940  bj-fast  12941  bj-stand  12945  bj-trdc  12948  bj-fadc  12949  decidr  12992  djulclALT  12997  djurclALT  12998  bj-indind  13119  bj-2inf  13125  bj-nntrans2  13139  bj-peano4  13142  bj-nnord  13145  bj-inf2vn  13161  bj-inf2vn2  13162  bj-findis  13166  pwf1oexmid  13183  exmid1stab  13184  subctctexmid  13185  nnsf  13188  nninfsellemdc  13195  nninffeq  13205  exmidsbthrlem  13206  sbthom  13210  triap  13213  trilpo  13225