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 )

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  10847  frec2uzrand  10857  frec2uzf1od  10858  frecuzrdgrcl  10862  frecuzrdgtcl  10864  frecuzrdgrclt  10867  frecuzrdgfunlem  10871  frecfzennn  10878  nninfinf  10895  seq3f1olemp  10967  seq3f1oleml  10968  seqf1oglem1  10971  ser0f  10986  expcl2lemap  11003  hashunsng  11264  hashmap  11284  sshashneg  11297  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  iswrdinn0  11325  snopiswrd  11330  wrdlndm  11337  iswrdsymb  11338  wrdsymb1  11357  ccatfv0  11387  ccatval21sw  11389  lswccatn0lsw  11395  eqs1  11412  ccat1st1st  11425  lswccats1fst  11428  fzowrddc  11435  swrdfv0  11442  swrdlen2  11450  swrdfv2  11451  swrdsbslen  11454  swrdspsleq  11455  pfxfv0  11480  pfxtrcfv0  11482  pfxeq  11484  pfx1  11491  swrdswrdlem  11492  cats1un  11509  pfxccatin12lem2a  11515  pfxccatin12lem2  11519  pfxccatin12lem3  11520  swrdccat  11523  cats1fvn  11552  cats1fvnd  11553  shftfvalg  11599  shftfval  11602  caucvgre  11763  rexanuz  11770  recvguniq  11777  rennim  11784  resqrexlemf  11789  rsqrmo  11809  fimaxre2  12010  climeu  12081  sumdc  12143  summodc  12169  zsumdc  12170  isum  12171  fisumss  12178  isumss2  12179  fsumsplit  12193  sumsnf  12195  fsumsplitsn  12196  sumtp  12200  sumsplitdc  12218  fsum2dlemstep  12220  fisum0diag2  12233  fsumconst  12240  modfsummodlemstep  12243  fsum00  12248  fsumabs  12251  fsumiun  12263  isumlessdc  12282  expcnv  12290  prodmodc  12364  zproddc  12365  iprodap  12366  iprodap0  12368  fprodssdc  12376  prodsnf  12378  fprodsplitdc  12382  fprodsplit  12383  fprodm1  12384  fprod1p  12385  fprodunsn  12390  fprod2dlemstep  12408  fprodsplitsn  12419  ef0lem  12446  modmulconst  12609  dvdsdivcl  12636  dvdsssfz1  12638  dvdsfac  12646  zeoxor  12655  nn0ehalf  12689  nn0oddm1d2  12695  nnoddm1d2  12696  divalglemeunn  12707  divalglemeuneg  12709  bitsfzolem  12740  bitsinv1  12748  gcdsupex  12753  gcdsupcl  12754  bezoutlemnewy  12792  bezoutlemmain  12794  bezoutlemeu  12803  dfgcd2  12810  nnwosdc  12835  nninfct  12837  algrf  12842  algcvgblem  12846  lcmgcdlem  12874  lcmdvds  12876  coprmgcdb  12885  mulgcddvds  12891  qredeu  12894  cncongr1  12900  cncongr2  12901  isprm2lem  12913  dvdsnprmd  12922  prmdc  12927  prmdcz  12928  oddprmge3  12933  pwbdvdseu  12966  nn0sqdcq  13007  phibndlem  13017  dfphi2  13021  hashdvds  13022  phiprmpw  13023  eulerthlemh  13032  hashgcdeq  13041  phisum  13042  odzdvds  13047  reumodprminv  13055  nnnn0modprm0  13057  prm23ge5  13066  pclemdc  13090  pcdvdsb  13122  difsqpwdvds  13140  oddprmdvds  13156  1arith  13169  4sqlem3  13192  4sqlemafi  13197  4sqlemffi  13198  4sqleminfi  13199  4sqexercise1  13200  4sqlem11  13203  4sqlem19  13211  ballotfilemcdc  13275  ballotfilemdifcfi  13277  ballotfilemdifcfz  13279  ballotfilem2  13280  ballotfilemiex  13296  ballotfilemscl  13299  ballotfilemth  13333  ennnfonelemdc  13342  ennnfonelemh  13347  ennnfonelemhf1o  13356  ennnfonelemf1  13361  ennnfonelemrn  13362  ennnfonelemdm  13363  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctiunctlemudc  13380  ctiunctlemf  13381  ctiunctal  13384  nninfdclemcl  13391  nninfdclemf  13392  nninfdclemp1  13393  isstructim  13418  setsresg  13442  strleund  13510  1strbas  13524  2strbasg  13527  2stropg  13528  restsspw  13656  tgval  13669  ptex  13671  imasaddfnlemg  13688  fnpr2o  13713  fnpr2ob  13714  mgmidsssn0  13757  fngzsum  13761  gzsumvalx  13762  isnsgrp  13774  sgrpidmndm  13786  mndinvmod  13811  mnd1  13815  mhmeql  13852  grpinveu  13896  mulgval  13978  subgintm  14054  trivsubgsnd  14057  eqgfval  14078  ecqusaddd  14094  ecqusaddcl  14095  ghmeql  14123  iscmnd  14185  imasabl  14224  gzsummhm2  14230  gsump1  14241  gsummhm2fi  14249  prdsinvlem  14280  rnglz  14328  srgfcl  14361  rhmopp  14567  opprlring  14588  subrgdvds  14627  lssuni  14784  lssintclm  14805  lspf  14810  qusmulrng  14953  mulgrhm2  15029  znf1o  15070  aspid  15101  psrbagfi  15143  psrbagconcl  15148  psr1clfi  15170  mplsubgfilemcl  15181  istopon  15205  toponcom  15219  topgele  15221  topontopn  15229  tsettps  15230  eltg2b  15246  unitg  15254  tgss2  15271  bastop2  15276  distop  15277  epttop  15282  cldss2  15298  neisspw  15340  neipsm  15346  neiuni  15353  tgcn  15400  tgcnp  15401  cnntr  15417  lmff  15441  txuni2  15448  txbasex  15449  txbas  15450  txcnp  15463  txcnmpt  15465  txcn  15467  txdis  15469  txdis1cn  15470  cnmpt11  15475  cnmpt12  15479  cnmpt21  15483  cnmpt2t  15485  cnmpt22  15486  blsscls2  15685  xmetxpbl  15700  xmettxlem  15701  tgqioo  15747  fsumcncntop  15759  cncfmpt1f  15790  mulcncflem  15799  mulcncf  15800  dedekindeu  15815  dedekindicclemicc  15824  dedekindicc  15825  ivthinclemdisj  15832  hovercncf  15838  limcimo  15857  cnmptlimc  15866  reldvg  15871  dvfvalap  15873  dvfgg  15880  dvmptfsum  15917  dveflem  15918  dvef  15919  elply2  15927  sincn  15961  coscn  15962  reeff1o  15965  pilem3  15976  ioocosf1o  16047  ppiqfi  16203  prmdvdsfi  16204  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  chtdif  16225  efchtqdvds  16226  ppidif  16230  prmorcht  16243  mpodvdsmulf1o  16245  fsumdvdsmul  16246  ppiqub  16254  perfectlem2  16261  bcmono  16265  bpos  16281  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  lgseisenlem2  16356  lgseisenlem3  16357  lgsquadlem2  16363  2lgslem3  16386  2sqlem2  16400  mul2sq  16401  2sqlem3  16402  2sqlem7  16406  edgstruct  16471  pw0ss  16490  incistruhgr  16497  upgrex  16510  umgrnloop0  16524  upgr1een  16531  lfgrnloopen  16540  umgredg  16552  umgrnloop2  16558  uspgredgiedg  16585  uspgriedgedg  16586  usgrislfuspgrdom  16597  usgredg3  16621  uspgredg2vlem  16627  uspgredg2v  16628  ushgredgedg  16633  ushgredgedgloop  16635  uhgr0vsize0en  16642  usgr1e  16648  subusgr  16682  vtxedgfi  16696  vtxlpfi  16697  vtxdumgrfival  16705  1loopgrvd2fi  16712  p1evtxdeqfilem  16718  vdegp1aid  16721  wlkcprim  16757  wlk1walkdom  16766  uspgr2wlkeq  16772  upgr2wlkdc  16784  wlkres  16786  clwwlkccatlem  16807  clwwlknp  16824  umgr2cwwk2dif  16831  trlsegvdegfi  16874  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lembfi  16884  depindlem1  16913  bj-trst  16933  bj-fast  16935  bj-stand  16942  bj-trdc  16946  bj-fadc  16948  decidr  16990  djulclALT  16995  djurclALT  16996  bj-charfunr  17002  bj-indind  17124  bj-2inf  17130  bj-nntrans2  17144  bj-peano4  17147  bj-nnord  17150  bj-inf2vn  17166  bj-inf2vn2  17167  bj-findis  17171  pwf1oexmid  17195  subctctexmid  17196  pw1dceq  17201  exmidnotnotr  17202  exmidcon  17203  exmidpeirce  17204  wexmiddc  17208  wexmiddiffi  17210  wexmiddifxylem  17211  wexmiddifxy  17212  nnsf  17214  nninfsellemdc  17219  nninffeq  17229  nnnninfen  17230  exmidsbthrlem  17233  sbthom  17237  triap  17244  trilpo  17259  apdifflemr  17263  redcwlpo  17272  tridceq  17273  nconstwlpolem0  17280  nconstwlpolem  17282  nconstwlpo  17283  neapmkv  17285  ltlenmkv  17287