Theorem mpbird 167

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbird.min	|- ( ph -> ch )
mpbird.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbird	|- ( ph -> ps )

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 |- ( ph -> ch )
2		mpbird.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 158	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mpd 13	1 |- ( ph -> ps )

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:  mpbiri  168  pm5.19  707  pm4.55dc  940  mpbir2and  946  pm3.12dc  960  mpbir3and  1182  pm5.15dc  1400  eqeltrd  2270  eqnetrd  2388  3netr4d  2397  r19.30dc  2641  raleqtrrdv  2700  rexeqtrrdv  2701  sbcne12g  3098  eqsstrd  3215  3sstr4d  3224  eqbrtrd  4051  3brtr4d  4061  snelpwi  4241  prelpwi  4243  pwel  4247  ordelon  4414  onin  4417  elelsuc  4440  onsuc  4533  onsucb  4535  onintonm  4549  omsinds  4654  sosng  4732  relssdv  4751  eqbrrdv  4756  eqrelrdv2  4758  relsnopg  4763  breldmg  4868  elrnmptdv  4916  iss  4988  xpimasn  5114  elxp4  5153  elxp5  5154  iotam  5246  funssres  5296  f0rn0  5448  fimadmfo  5485  sefvex  5575  fvun1  5623  eqfnfvd  5658  fvimacnvi  5672  fvimacnv  5673  fvelrn  5689  fmpt3d  5714  fmpt2d  5720  resflem  5722  fmptco  5724  fsn  5730  ftpg  5742  fconst2g  5773  funfvima3  5792  elabrexg  5801  foeqcnvco  5833  f1eqcocnv  5834  fliftfun  5839  fliftfund  5840  fliftval  5843  riota5f  5898  f1ofveu  5906  f1ocnvd  6120  f1opw2  6124  off  6143  offval2  6146  ofrfval2  6147  caofref  6154  caofinvl  6155  elxp6  6222  cnvf1olem  6277  f2ndf  6279  f1od2  6288  tposf12  6322  smores2  6347  tfrlemisucaccv  6378  tfrlemibfn  6381  tfr1onlemsucaccv  6394  tfr1onlembfn  6397  tfrcllemsucaccv  6407  tfrcllembfn  6410  tfrcl  6417  tfri3  6420  frecabcl  6452  nnsucsssuc  6545  ersym  6599  ertr  6602  swoer  6615  erth  6633  riinerm  6662  qliftfund  6672  eroprf  6682  ecopoverg  6690  th3qlem1  6691  elmapssres  6727  mapss  6745  fdiagfn  6746  ixpssmap2g  6781  mapsnf1o  6791  f1dom2g  6810  dom3d  6828  pw2f1odclem  6890  fopwdom  6892  mapxpen  6904  nndomo  6920  dif1en  6935  findcard2  6945  findcard2s  6946  diffisn  6949  fimax2gtrilemstep  6956  fientri3  6971  fiintim  6985  opabfi  6992  f1dmvrnfibi  7003  sbthlemi6  7021  elfir  7032  fifo  7039  supelti  7061  supsnti  7064  cnvinfex  7077  ordiso2  7094  updjud  7141  djudom  7152  difinfsn  7159  ctssdc  7172  enumctlemm  7173  enumct  7174  nninfninc  7182  enomnilem  7197  fodjuf  7204  ismkvnex  7214  omnimkv  7215  enmkvlem  7220  enwomnilem  7228  nninfdcinf  7230  nninfwlporlem  7232  isnumi  7242  exmidfodomrlemrALT  7263  djudoml  7279  djudomr  7280  netap  7314  2omotaplemap  7317  2omotaplemst  7318  exmidapne  7320  cc2lem  7326  cc3  7328  ltsopi  7380  pitri3or  7382  ltdcpi  7383  indpi  7402  enqdc  7421  enqdc1  7422  addcmpblnq  7427  mulcanenq  7445  recrecnq  7454  nqtri3or  7456  ltdcnq  7457  ltsonq  7458  ltaddnq  7467  subhalfnqq  7474  archnqq  7477  prarloclemarch2  7479  enq0tr  7494  nqnq0  7501  addcmpblnq0  7503  mulcanenq0ec  7505  nnnq0lem1  7506  nqpnq0nq  7513  nq0m0r  7516  nq02m  7525  prarloclemlt  7553  prarloclemcalc  7562  addlocpr  7596  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  prmuloclemcalc  7625  mullocprlem  7630  mulnqprlemrl  7633  mulnqprlemru  7634  1idprl  7650  1idpru  7651  ltaddpr  7657  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemdisj  7666  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  addcanprg  7676  prplnqu  7680  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  aptiprleml  7699  aptiprlemu  7700  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlem1  7719  cauappcvgprlem2  7720  caucvgprlemnkj  7726  caucvgprlemopl  7729  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemnkltj  7749  caucvgprprlemopl  7757  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  caucvgprprlemaddq  7768  caucvgprprlem2  7770  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemloc  7781  suplocexprlemlub  7784  prsrlem1  7802  0idsr  7827  1idsr  7828  recexgt0sr  7833  archsr  7842  prsradd  7846  caucvgsrlemcau  7853  caucvgsrlembound  7854  caucvgsrlemoffgt1  7859  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  pitonnlem1p1  7906  pitonn  7908  pitoregt0  7909  peano2nnnn  7913  recidpirq  7918  axcaucvglemval  7957  leid  8103  nltled  8140  readdcan  8159  addneintrd  8207  addneintr2d  8208  pncan  8225  subsub2  8247  subsub4  8252  negned  8327  subne0d  8339  subneintrd  8374  subneintr2d  8376  subeq0bd  8398  subdi  8404  gt0add  8592  rimul  8604  rereim  8605  ltmul1a  8610  apreim  8622  apirr  8624  mulap0r  8634  msqge0  8635  mulge0  8638  gt0ap0  8645  ltap  8652  subap0d  8663  recexaplem2  8671  mulap0bad  8678  mulap0bbd  8679  mul0eqap  8689  divrecap  8707  div0ap  8721  div1  8722  recrecap  8728  divdivdivap  8732  ddcanap  8745  rerecclap  8749  div2negap  8754  diveqap1bd  8855  recgt0  8869  prodgt0  8871  lemul1a  8877  recp1lt1  8918  squeeze0  8923  peano2nn  8994  div4p1lem1div2  9236  arch  9237  peano2z  9353  peano2zm  9355  ztri3or  9360  nn0n0n1ge2  9387  zextle  9408  gtndiv  9412  suprzclex  9415  nn0ind-raph  9434  uzid  9606  uzneg  9611  uztric  9614  uz11  9615  eluzp1l  9617  qdivcl  9708  irrmul  9712  irrmulap  9713  rpnegap  9752  negelrpd  9754  ledivge1le  9792  mul2lt0rlt0  9825  mul2lt0rgt0  9826  nn0ledivnn  9833  ltpnf  9846  mnflt  9849  pnfge  9855  mnfle  9858  xrlttr  9861  xrltso  9862  xrlttri3  9863  xrleid  9866  xaddass2  9936  xltadd1  9942  xlt2add  9946  xleaddadd  9953  iccf1o  10070  fztri3or  10105  fznlem  10107  fzn  10108  fzsplit2  10116  fznatpl1  10142  uzsplit  10158  fseq1p1m1  10160  fzm1  10166  fznn0sub2  10194  difelfznle  10201  1fv  10205  fzodcel  10219  fzospliti  10243  fzouzsplit  10246  eluzgtdifelfzo  10264  exfzdc  10307  subfzo0  10309  exbtwnz  10319  qbtwnrelemcalc  10324  flqlelt  10345  qfraclt1  10349  qfracge0  10350  flqltnz  10356  btwnzge0  10369  flhalf  10371  fldiv4lem1div2uz2  10375  ceiqle  10384  intfracq  10391  mulqmod0  10401  modqge0  10403  modqlt  10404  modqid  10420  modqid0  10421  m1modge3gt1  10442  modqltm1p1mod  10447  q2txmodxeq0  10455  modaddmodlo  10459  modsumfzodifsn  10467  addmodlteq  10469  frecuzrdgtcl  10483  frecuzrdgtclt  10492  uzennn  10507  uzsinds  10515  seqf  10535  seqf2  10539  monoord2  10557  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seq3f1olemqsumkj  10582  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1oleml  10587  seqf1oglem1  10590  ser3le  10608  exp3vallem  10611  exp3val  10612  expp1  10617  expcllem  10621  ltexp2a  10662  leexp2a  10663  nn0ltexp2  10780  faclbnd  10812  faclbnd2  10813  faclbnd3  10814  bcval5  10834  bcpasc  10837  hashennn  10851  fihasheqf1oi  10858  hashsng  10869  fihashfn  10871  hashun  10876  fihashss  10887  fihashssdif  10889  hashfz  10892  hashxp  10897  fimaxq  10898  zfz1isolem1  10911  seq3coll  10913  wrdf  10920  wrdlenge2n0  10949  fstwrdne0  10953  wrdred1hash  10957  shftfn  10968  cjth  10990  cjmulrcl  11031  reim0bd  11088  rerebd  11089  cjrebd  11090  caucvgre  11125  cvg1nlemcxze  11126  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniq  11139  resqrexlemover  11154  resqrexlemdec  11155  resqrexlemgt0  11164  resqrexlemoverl  11165  resqrexlemglsq  11166  rersqrtthlem  11174  sqrtgt0  11178  leabs  11218  absexpzap  11224  absle  11233  recvalap  11241  abstri  11248  abs2dif  11250  amgm2  11262  absne0d  11331  maxleim  11349  maxabslemab  11350  maxabslemlub  11351  maxltsup  11362  zmaxcl  11368  fimaxre2  11370  minmax  11373  rpmincl  11381  bdtrilem  11382  bdtri  11383  xrmaxleim  11387  xrmaxiflemcom  11392  xrmaxltsup  11401  xrmaxadd  11404  xrminmax  11408  xrminrpcl  11417  climconst  11433  climuni  11436  2clim  11444  climcn1  11451  climcn2  11452  reccn2ap  11456  climge0  11468  climle  11477  climsqz  11478  climsqz2  11479  serf0  11495  summodclem3  11523  summodclem2a  11524  fsumcl2lem  11541  sumpr  11556  sumtp  11557  fsum0diaglem  11583  mptfzshft  11585  fsumle  11606  fsumlt  11607  divcnv  11640  trireciplem  11643  expcnvap0  11645  expcnv  11647  explecnv  11648  geosergap  11649  cvgratnnlembern  11666  cvgratnnlemabsle  11670  cvgratnnlemsumlt  11671  cvgratz  11675  cvgratgt0  11676  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  clim2divap  11683  prodmodclem3  11718  prodmodclem2a  11719  fprodseq  11726  fprodmul  11734  fprodfac  11758  fprodconst  11763  fprodap0  11764  fprodap0f  11779  fprodle  11783  eftcl  11797  ef0lem  11803  efsub  11824  eftlub  11833  eflegeo  11844  tanval2ap  11856  sinadd  11879  cos2t  11893  cos2tsin  11894  sin01bnd  11900  cos01bnd  11901  eirraplem  11920  dvdsval2  11933  dvdsdc  11941  dvds0lem  11944  zdvdsdc  11955  dvdscmulr  11963  dvdsmulcr  11964  dvdslelemd  11985  divconjdvds  11991  dvdsext  11997  fzm1ndvds  11998  dvdsmod  12004  oexpneg  12018  2tp1odd  12025  mulsucdiv2z  12026  2teven  12028  zeo5  12029  opeo  12038  omeo  12039  nn0ob  12049  divalglemnqt  12061  zsupcllemstep  12082  zsupcl  12084  zssinfcl  12085  infssuzex  12086  infssuzcldc  12088  suprzubdc  12089  nninfdcex  12090  gcddvds  12100  dvdslegcd  12101  gcdneg  12119  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlema  12136  bezoutlemb  12137  bezoutlemmo  12143  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  bezout  12148  dfgcd2  12151  uzwodc  12174  lcmcllem  12205  lcmneg  12212  lcmgcdlem  12215  lcmdvds  12217  lcmid  12218  3lcm2e6woprm  12224  6lcm4e12  12225  ncoprmgcdne1b  12227  mulgcddvds  12232  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  isprm2lem  12254  prmind2  12258  dvdsnprmd  12263  prm2orodd  12264  sqnprm  12274  isprm5lem  12279  rpexp  12291  sqrt2irrlem  12299  oddpwdclemdc  12311  sqrt2irraplemnn  12317  qnumdencoprm  12331  qeqnumdivden  12332  nn0gcdsq  12338  nn0sqrtelqelz  12344  nonsq  12345  phicl2  12352  phibnd  12355  hashdvds  12359  phiprmpw  12360  phimullem  12363  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemth  12370  prmdiveq  12374  hashgcdlem  12376  odzdvds  12383  modprminv  12387  nnnn0modprm0  12393  modprmn0modprm0  12394  pythagtriplem10  12407  pythagtriplem19  12420  pythagtrip  12421  pcpre1  12430  pcpremul  12431  pceu  12433  pcmul  12439  pcdiv  12440  pcqmul  12441  pcqdiv  12445  pcexp  12447  pcdvdsb  12458  pcidlem  12461  pcdvdstr  12465  pcgcd1  12466  pc2dvds  12468  pcprmpw2  12471  difsqpwdvds  12476  pcaddlem  12477  pcadd  12478  pcadd2  12479  pcmpt  12481  pcmptdvds  12483  pcprod  12484  fldivp1  12486  pcfaclem  12487  pcfac  12488  pcbc  12489  qexpz  12490  pockthlem  12494  pockthg  12495  1arithlem4  12504  1arith  12505  1arith2  12506  4sqlem6  12521  4sqlem8  12523  4sqlem9  12524  4sqlem10  12525  4sqexercise1  12536  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  4sqlem12  12540  4sqlem15  12543  4sqlem16  12544  4sqlem17  12545  znnen  12555  ennnfonelemk  12557  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemrnh  12573  ennnfonelemfun  12574  ennnfonelemf1  12575  ennnfonelemrn  12576  ennnfonelemnn0  12579  ctinfomlemom  12584  ctiunctlemudc  12594  unct  12599  omctfn  12600  ssnnctlemct  12603  nninfdclemp1  12607  nninfdc  12610  structfung  12635  setsfun  12653  setsfun0  12654  setscom  12658  setsslid  12669  imasaddfnlemg  12897  imasaddvallemg  12898  mgmsscl  12944  plusffng  12948  mgmplusf  12949  mgm0  12952  mgm1  12953  opifismgmdc  12954  gsumfzval  12974  gsumprval  12982  sgrp1  12994  issgrpd  12995  mndpfo  13019  mndfo  13020  mnd1  13027  0subm  13056  mhmima  13063  grpinvfng  13116  isgrpinv  13126  grpinvid  13132  grpinvf1o  13142  grpinvadd  13150  grpsubf  13151  grpsubsub4  13165  grplactcnv  13174  grp1  13178  grp1inv  13179  qusgrp2  13183  mulgfng  13194  subginv  13251  resgrpisgrp  13265  subgintm  13268  0subg  13269  0nsg  13284  qusinv  13306  ghminv  13320  ghmrn  13327  ghmeql  13337  ghmnsgima  13338  kerf1ghm  13344  conjnmz  13349  rngass  13435  rngmneg1  13443  rngmneg2  13444  qusrng  13454  srgideu  13468  srgidmlem  13474  srgpcomp  13486  srg1expzeq1  13491  ringcl  13509  ringideu  13513  ringidmlem  13518  ringnegl  13547  ringnegr  13548  ring1  13555  qusring2  13562  opprringbg  13576  dvdsrd  13590  dvdsr01  13600  isunitd  13602  unitinvcl  13619  unitinvinv  13620  unitnegcl  13626  rhmmul  13660  rhmf1o  13664  nzrunit  13684  lringuplu  13692  subrngintm  13708  subrgsubm  13730  subrgintm  13739  aprsym  13780  scaffng  13805  lmodscaf  13806  lsssn0  13866  lss1d  13879  lssintclm  13880  lspval  13886  lspcl  13887  lspsnid  13903  lspprid1  13907  lspsn  13912  sraval  13933  rspcl  13987  rspssid  13988  rspssp  13990  rnglidlmmgm  13992  rnglidlmsgrp  13993  cnfldneg  14061  zringinvg  14092  expghmap  14095  znzrhfo  14136  znf1o  14139  znhash  14144  znidomb  14146  znrrg  14148  psraddcl  14164  baspartn  14218  eltg3i  14224  tgclb  14233  topbas  14235  2basgeng  14250  topcld  14277  0cld  14280  uncld  14281  neif  14309  elnei  14320  0nei  14334  restbasg  14336  iscnp4  14386  cnpnei  14387  cnclima  14391  cncnp  14398  cnrest2r  14405  cndis  14409  lmff  14417  lmtopcnp  14418  txbas  14426  txopn  14433  txcnp  14439  upxp  14440  txdis1cn  14446  cnmpt11  14451  cnmpt21  14459  psmetge0  14499  xmetge0  14533  xmettpos  14538  xmetrtri  14544  metrtri  14545  xblpnfps  14566  xblpnf  14567  blfps  14577  blf  14578  ssblps  14593  ssbl  14594  blbas  14601  metss2  14666  xmettxlem  14677  xmettx  14678  qtopbas  14690  divcnap  14723  cncfss  14738  cdivcncfap  14758  expcncf  14763  cnopnap  14765  maxcncf  14769  mincncf  14770  dedekindeulemuub  14771  dedekindeulemlu  14775  dedekindeu  14777  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemlu  14784  dedekindicclemicc  14786  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthinc  14797  ivthreinc  14799  hoverlt1  14803  ellimc3apf  14814  limcimolemlt  14818  limcimo  14819  limcresi  14820  cnplimclemle  14822  reldvg  14833  dvfgg  14842  dvidlemap  14845  dvcjbr  14857  dvcj  14858  dvrecap  14862  dveflem  14872  dvef  14873  elply2  14881  elplyr  14886  reeff1oleme  14907  pilem3  14918  sinq34lt0t  14966  cosq14gt0  14967  coseq0q4123  14969  tangtx  14973  sincosq1eq  14974  cosordlem  14984  logdivlti  15016  relogbval  15083  relogbzcl  15084  nnlogbexp  15091  logbgcd1irr  15099  logbgcd1irraplemexp  15100  logbgcd1irraplemap  15101  wilthlem1  15112  zabsle1  15115  lgslem1  15116  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgsval2lem  15126  lgscl1  15139  lgsmod  15142  lgsdir2lem5  15148  lgsdir2  15149  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  gausslemma2dlem0c  15167  gausslemma2dlem0h  15172  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem3  15179  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  2lgsoddprmlem2  15194  2sqlem3  15204  2sqlem8  15210  2sqlem10  15212  fnmptd  15296  bj-sels  15406  bj-nnelon  15451  pwle2  15489  pwf1oexmid  15490  pw1nct  15493  nninfall  15499  nninfsellemdc  15500  nninfself  15503  refeq  15518  isomninnlem  15520  cvgcmp2nlemabs  15522  trilpolemlt1  15531  trirec0  15534  apdifflemf  15536  apdifflemr  15537  apdiff  15538  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  reap0  15548  cndcap  15549