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	|- ( 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 133	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

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  oibabs  714  dcim  841  dcstab  844  stdcndc  845  stdcndcOLD  846  dcor  935  3mix1  1166  3mix2  1167  3jca  1177  syl3anbrc  1181  syl21anbrc  1182  inegd  1372  pclem6  1374  xoranor  1377  nfxfrd  1473  nfd  1521  hban  1545  nfan1  1562  nford  1565  nfand  1566  hbim1  1568  nfal  1574  alexim  1643  nnal  1647  ax6blem  1648  nf4r  1669  19.34  1682  nfexd  1759  sbcof2  1808  nfsb2or  1835  sbidm  1849  nfdv  1875  nfd2  2020  nfeudv  2039  mon  2053  eumo  2056  mo23  2065  eu2  2068  eu3h  2069  exmodc  2074  exmonim  2075  mo2r  2076  mo3h  2077  bm1.1  2160  eqrdv  2173  3eltr4g  2261  abbi2dv  2294  abbi1dv  2295  nfcd  2312  nfcxfrd  2315  dcned  2351  neqned  2352  3netr4g  2380  necon3bi  2395  necon2ai  2399  nnral  2465  alral  2520  rspe  2524  rsp2e  2526  rgen2a  2529  ralrimi  2546  r19.27v  2602  r19.28v  2603  r19.27av  2610  r19.32r  2621  nfreudxy  2648  mormo  2686  nrexrmo  2691  cgsex2g  2771  cgsex4g  2772  spc2egv  2825  spc2gv  2826  spc3egv  2827  spc3gv  2828  rspce  2834  ceqex  2862  elrab3t  2890  elrabd  2893  mosubt  2912  mo2icl  2914  reu3  2925  reu6i  2926  2rmorex  2941  sbc5  2984  rspesbca  3045  rmo2ilem  3050  sbnfc2  3115  ssrd  3158  ssrdv  3159  3sstr4g  3196  eqsstrid  3199  ss2abdv  3226  abssdv  3227  rabssdv  3233  ss2rabdv  3234  ssun1  3296  unssad  3310  unssbd  3311  ssddif  3367  uneqin  3384  indifdir  3389  undif3ss  3394  reuss2  3413  n0rf  3433  reximdva0m  3436  rabxmdc  3452  ssindif0im  3480  minel  3482  ralidm  3521  ralm  3525  dcun  3531  ifmdc  3571  disjsn2  3652  absneu  3661  rabsneu  3662  opprc  3795  elunii  3810  dfnfc2  3823  uniss2  3836  unidif  3837  ssunieq  3838  intab  3869  iunss2  3927  iunxdif2  3930  invdisj  3992  disjiun  3993  3brtr4g  4032  trin  4106  triun  4109  truni  4110  trint  4111  iinexgm  4149  class2seteq  4158  pwuni  4187  exmid1dc  4195  exmidn0m  4196  exmidsssn  4197  exmid0el  4199  exmidel  4200  exmidundif  4201  exmidundifim  4202  mss  4220  copsex2t  4239  euotd  4248  pwunim  4280  ispod  4298  sotricim  4317  exse  4330  frind  4346  trssord  4374  suctr  4415  pwnex  4443  eusvnf  4447  eusvnfb  4448  eusv2nf  4450  rexxfrd  4457  ralxfr2d  4458  rexxfr2d  4459  rabxfrd  4463  reuhypd  4465  eldifpw  4471  iunpw  4474  ssorduni  4480  sucelon  4496  onsucelsucr  4501  sucunielr  4503  ontriexmidim  4515  ordtri2or2exmidlem  4519  onsucelsucexmid  4523  reg2exmidlema  4527  setindel  4531  elirr  4534  orddisj  4539  en2lp  4547  suc11g  4550  ordsuc  4556  nlimsucg  4559  ordtri2or2exmid  4564  ontri2orexmidim  4565  zfregfr  4567  wessep  4571  tfi  4575  peano5  4591  limom  4607  peano2b  4608  nndceq0  4611  nnpredcl  4616  0nelrel  4666  eqrelrdv  4716  xpsspw  4732  relint  4744  relop  4770  eqbrrdva  4790  opeldm  4823  elres  4936  relssres  4938  exse2  4995  issref  5003  trin2  5012  dminss  5035  imainss  5036  rnxpid  5055  dmsn0el  5090  dmmptg  5118  relrelss  5147  cnviinm  5162  iotanul  5185  sniota  5199  dffun5r  5220  funmo  5223  funco  5248  funun  5252  funprg  5258  funtpg  5259  funtp  5261  fntpg  5264  fununi  5276  funcnvuni  5277  imadiflem  5287  imainlem  5289  funimaexglem  5291  isarep2  5295  fnunsn  5315  2elresin  5319  fnimadisj  5328  dmmptd  5338  fco  5373  funssxp  5377  fssres  5383  feu  5390  fimacnvdisj  5392  fabexg  5395  f00  5399  f0rn0  5402  f1co  5425  fores  5439  foco  5440  f1ores  5468  foimacnv  5471  f1oun  5473  fun11iun  5474  f1oco  5476  fo00  5489  brprcneu  5500  fv3  5530  relelfvdm  5539  nfvres  5540  nfunsn  5541  funfvbrb  5621  respreima  5636  dff2  5652  dff3im  5653  dffo4  5656  fvmptelcdm  5661  ffvresb  5671  f1oresrab  5673  fmptco  5674  fsn  5680  fpr  5690  ftpg  5692  fsnunf  5708  fsnunfv  5709  elabrex  5749  dff1o6  5767  foeqcnvco  5781  fliftel1  5785  isores1  5805  isoini2  5810  riotasbc  5836  acexmidlemph  5858  acexmidlemcase  5860  oprabidlem  5896  brabvv  5911  eloprabga  5952  fnoprabg  5966  caovimo  6058  oprabexd  6118  fo1stresm  6152  fo2ndresm  6153  unielxp  6165  1st2ndbr  6175  fmpoco  6207  1stconst  6212  2ndconst  6213  poxp  6223  spc2ed  6224  disjxp1  6227  reldmtpos  6244  tposfun  6251  dftpos4  6254  smores  6283  smores2  6285  tfrlem1  6299  tfr0dm  6313  tfrlemibxssdm  6318  tfrlemibex  6320  tfrlemiubacc  6321  tfrlemi14d  6324  tfrexlem  6325  tfri1d  6326  tfr1onlembxssdm  6334  tfr1onlembex  6336  tfr1onlemubacc  6337  tfr1onlemres  6340  tfrcllemsucfn  6344  tfrcllembxssdm  6347  tfrcllembex  6349  tfrcllemubacc  6350  tfrcllemres  6353  tfri3  6358  rdgon  6377  frecabcl  6390  frecfcllem  6395  frecrdg  6399  2oconcl  6430  nnsucelsuc  6482  nntri3or  6484  nndceq  6490  nndcel  6491  dcdifsnid  6495  ecexr  6530  brdifun  6552  ecelqsdm  6595  iinerm  6597  eroveu  6616  erovlem  6617  ecopovtrn  6622  ecopovtrng  6625  th3qlem1  6627  pmsspw  6673  map0b  6677  mapsn  6680  mapsncnv  6685  ixpf  6710  uniixp  6711  ixpexgg  6712  resixp  6723  f1oen3g  6744  ssdomg  6768  domtr  6775  snfig  6804  enpr2d  6807  xpf1o  6834  xpmapenlem  6839  php5dom  6853  fidceq  6859  nnfi  6862  fiunsnnn  6871  findcard  6878  findcard2  6879  findcard2s  6880  ac6sfi  6888  tridc  6889  fimax2gtri  6891  finexdc  6892  exmidpw  6898  exmidpweq  6899  nnwetri  6905  unsnfi  6908  unsnfidcex  6909  unsnfidcel  6910  undifdcss  6912  tpfidisj  6917  iunfidisj  6935  snexxph  6939  fidcenumlemrks  6942  sbthlem2  6947  sbthlemi3  6948  sbthlem7  6952  sbthlemi8  6953  fival  6959  dcfi  6970  supmoti  6982  djuss  7059  updjudhf  7068  updjud  7071  casefun  7074  caseinj  7078  omp1eomlem  7083  djufun  7093  djuinj  7095  ctssdccl  7100  ctfoex  7107  nnnninf  7114  nnnninfeq2  7117  nninfisollem0  7118  nninfisollemne  7119  nninfisollemeq  7120  nninfisol  7121  finomni  7128  exmidomniim  7129  exmidomni  7130  fodjuomnilemdc  7132  omniwomnimkv  7155  nninfdcinf  7159  nninfwlporlem  7161  nninfwlpoimlemg  7163  nninfwlpoim  7166  exmidonfinlem  7182  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  dju1en  7202  exmidontriimlem1  7210  exmidontriimlem3  7212  pw1on  7215  3nsssucpw1  7225  cc4f  7243  cc4n  7245  dmaddpqlem  7351  nqpi  7352  dmaddpq  7353  dmmulpq  7354  ltdcnq  7371  subhalfnqq  7388  enq0sym  7406  enq0ref  7407  enq0tr  7408  nqnq0pi  7412  nq0nn  7416  addnq0mo  7421  mulnq0mo  7422  nqpnq0nq  7427  nqnq0a  7428  nqnq0m  7429  npsspw  7445  elnp1st2nd  7450  prnmaxl  7462  prnminu  7463  prarloc  7477  genprndl  7495  genprndu  7496  nqprm  7516  nqprl  7525  nqpru  7526  addnqprlemrl  7531  addnqprlemru  7532  prmuloc  7540  mulnqprlemrl  7547  mulnqprlemru  7548  ltsopr  7570  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemopu  7577  lteupri  7591  recexprlemopl  7599  recexprlemopu  7601  recexprlemdisj  7604  archpr  7617  cauappcvgprlemdisj  7625  cauappcvgprlemladdrl  7631  cauappcvgprlem2  7634  caucvgprlemnbj  7641  caucvgprlemdisj  7648  caucvgprlemladdfu  7651  caucvgprlem2  7654  caucvgprprlemnbj  7667  caucvgprprlemdisj  7676  suplocexprlemml  7690  suplocexprlemrl  7691  suplocexprlemmu  7692  suplocexprlemloc  7695  addsrmo  7717  mulsrmo  7718  recexgt0sr  7747  prsrpos  7759  caucvgsrlemasr  7764  suplocsrlemb  7780  suplocsrlempr  7781  suplocsr  7783  elrealeu  7803  pitonn  7822  pitoregt0  7823  pitore  7824  recnnre  7825  axaddcl  7838  axaddrcl  7839  axmulcl  7840  axmulrcl  7841  axrnegex  7853  axcnre  7855  axpre-lttrn  7858  rereceu  7863  axarch  7865  axpre-suploclemres  7875  axpre-suploc  7876  ltxrlt  7997  apirr  8536  divmulasscomap  8625  rerecclap  8659  lbreu  8873  arch  9144  0mnnnnn0  9179  nnm1nn0  9188  elnnnn0c  9192  elnnz1  9247  ztri3or0  9266  nzadd  9276  nn0n0n1ge2  9294  zdceq  9299  zdcle  9300  zdclt  9301  uzind  9335  eluzge3nn  9543  supinfneg  9566  infsupneg  9567  eluz2b2  9574  elnn1uz2  9578  elnn0dc  9582  elnndc  9583  nn01to3  9588  znq  9595  qaddcl  9606  qmulcl  9608  qreccl  9613  irradd  9617  irrmul  9618  elpq  9619  cnref1o  9621  xnn0dcle  9771  xrpnfdc  9811  xrmnfdc  9812  xaddcom  9830  xnegdi  9837  xpncan  9840  xleadd1a  9842  iooidg  9878  elioo4g  9903  fzdcel  10008  fznlem  10009  fzpreddisj  10039  fz0to4untppr  10092  elfz0ubfz0  10093  elfz0fzfz0  10094  fz0fzelfz0  10095  fz0fzdiffz0  10098  elfzmlbp  10100  difelfzle  10102  4fvwrd4  10108  fzosplit  10145  elfzo0  10150  fzo1fzo0n0  10151  elfzonn0  10154  fzofzim  10156  elfzo1  10158  elfzom1elp1fzo  10170  fzossfzop1  10180  ssfzo12bi  10193  exfzdc  10208  qdceq  10215  exbtwnzlemstep  10216  exbtwnzlemex  10218  exbtwnz  10219  rebtwn2zlemstep  10221  rebtwn2z  10223  qbtwnxr  10226  modfzo0difsn  10363  frec2uzrand  10373  frec2uzf1od  10374  frecuzrdgrcl  10378  frecuzrdgtcl  10380  frecuzrdgrclt  10383  frecuzrdgfunlem  10387  frecfzennn  10394  seq3f1olemp  10470  seq3f1oleml  10471  ser0f  10483  expcl2lemap  10500  hashunsng  10753  shftfvalg  10793  shftfval  10796  caucvgre  10956  rexanuz  10963  recvguniq  10970  rennim  10977  resqrexlemf  10982  rsqrmo  11002  fimaxre2  11201  climeu  11270  sumdc  11332  summodc  11357  zsumdc  11358  isum  11359  fisumss  11366  isumss2  11367  fsumsplit  11381  sumsnf  11383  fsumsplitsn  11384  sumtp  11388  sumsplitdc  11406  fsum2dlemstep  11408  fisum0diag2  11421  fsumconst  11428  modfsummodlemstep  11431  fsum00  11436  fsumabs  11439  fsumiun  11451  isumlessdc  11470  expcnv  11478  prodmodc  11552  zproddc  11553  iprodap  11554  iprodap0  11556  fprodssdc  11564  prodsnf  11566  fprodsplitdc  11570  fprodsplit  11571  fprodm1  11572  fprod1p  11573  fprodunsn  11578  fprod2dlemstep  11596  fprodsplitsn  11607  ef0lem  11634  modmulconst  11796  dvdsdivcl  11821  dvdsssfz1  11823  dvdsfac  11831  zeoxor  11839  nn0ehalf  11873  nn0oddm1d2  11879  nnoddm1d2  11880  divalglemeunn  11891  divalglemeuneg  11893  zsupcllemstep  11911  infssuzex  11915  gcdsupex  11923  gcdsupcl  11924  bezoutlemnewy  11962  bezoutlemmain  11964  bezoutlemeu  11973  dfgcd2  11980  nnwosdc  12005  algrf  12010  algcvgblem  12014  lcmgcdlem  12042  lcmdvds  12044  coprmgcdb  12053  mulgcddvds  12059  qredeu  12062  cncongr1  12068  cncongr2  12069  isprm2lem  12081  dvdsnprmd  12090  prmdc  12095  oddprmge3  12100  pw2dvdseu  12133  phibndlem  12181  dfphi2  12185  hashdvds  12186  phiprmpw  12187  eulerthlemh  12196  hashgcdeq  12204  phisum  12205  odzdvds  12210  reumodprminv  12218  nnnn0modprm0  12220  prm23ge5  12229  pclemdc  12253  pcdvdsb  12284  difsqpwdvds  12302  oddprmdvds  12317  1arith  12330  4sqlem3  12353  ennnfonelemdc  12365  ennnfonelemh  12370  ennnfonelemhf1o  12379  ennnfonelemf1  12384  ennnfonelemrn  12385  ennnfonelemdm  12386  exmidunben  12392  ctinfomlemom  12393  ctinfom  12394  ctiunctlemudc  12403  ctiunctlemf  12404  ctiunctal  12407  nninfdclemcl  12414  nninfdclemf  12415  nninfdclemp1  12416  isstructim  12441  setsresg  12465  strleund  12517  1strbas  12528  2strbasg  12530  2stropg  12531  restsspw  12618  mgmidsssn0  12667  isnsgrp  12676  sgrpidmndm  12685  mndinvmod  12707  mnd1  12708  mhmeql  12736  grpinveu  12771  mulgval  12845  iscmnd  12897  srgfcl  12949  istopon  13062  toponcom  13076  topgele  13078  topontopn  13086  tsettps  13087  tgval  13100  eltg2b  13105  unitg  13113  tgss2  13130  bastop2  13135  distop  13136  epttop  13141  cldss2  13157  neisspw  13199  neipsm  13205  neiuni  13212  tgcn  13259  tgcnp  13260  cnntr  13276  lmff  13300  txuni2  13307  txbasex  13308  txbas  13309  txcnp  13322  txcnmpt  13324  txcn  13326  txdis  13328  txdis1cn  13329  cnmpt11  13334  cnmpt12  13338  cnmpt21  13342  cnmpt2t  13344  cnmpt22  13345  blsscls2  13544  xmetxpbl  13559  xmettxlem  13560  tgqioo  13598  fsumcncntop  13607  cncfmpt1f  13635  mulcncflem  13641  mulcncf  13642  dedekindeu  13652  dedekindicclemicc  13661  dedekindicc  13662  ivthinclemdisj  13669  limcimo  13685  cnmptlimc  13694  reldvg  13699  dvfvalap  13701  dvfgg  13708  dveflem  13738  dvef  13739  sincn  13741  coscn  13742  reeff1o  13745  pilem3  13755  ioocosf1o  13826  lgsne0  13990  2sqlem2  14002  mul2sq  14003  2sqlem3  14004  2sqlem7  14008  bj-trst  14031  bj-fast  14033  bj-stand  14040  bj-trdc  14044  bj-fadc  14046  decidr  14088  djulclALT  14093  djurclALT  14094  bj-charfunr  14102  bj-indind  14224  bj-2inf  14230  bj-nntrans2  14244  bj-peano4  14247  bj-nnord  14250  bj-inf2vn  14266  bj-inf2vn2  14267  bj-findis  14271  pwf1oexmid  14289  exmid1stab  14290  subctctexmid  14291  nnsf  14295  nninfsellemdc  14300  nninffeq  14310  exmidsbthrlem  14311  sbthom  14315  triap  14318  trilpo  14332  apdifflemr  14336  redcwlpo  14344  tridceq  14345  nconstwlpolem0  14351  nconstwlpolem  14353  nconstwlpo  14354  neapmkv  14356