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  2273  eqnetrd  2391  3netr4d  2400  r19.30dc  2644  raleqtrrdv  2703  rexeqtrrdv  2704  sbcne12g  3102  eqsstrd  3219  3sstr4d  3228  eqbrtrd  4055  3brtr4d  4065  snelpwi  4245  prelpwi  4247  pwel  4251  ordelon  4418  onin  4421  elelsuc  4444  onsuc  4537  onsucb  4539  onintonm  4553  omsinds  4658  sosng  4736  relssdv  4755  eqbrrdv  4760  eqrelrdv2  4762  relsnopg  4767  breldmg  4872  elrnmptdv  4920  iss  4992  xpimasn  5118  elxp4  5157  elxp5  5158  iotam  5250  funssres  5300  f0rn0  5452  fimadmfo  5489  sefvex  5579  fvun1  5627  eqfnfvd  5662  fvimacnvi  5676  fvimacnv  5677  fvelrn  5693  fmpt3d  5718  fmpt2d  5724  resflem  5726  fmptco  5728  fsn  5734  ftpg  5746  fconst2g  5777  funfvima3  5796  elabrexg  5805  foeqcnvco  5837  f1eqcocnv  5838  fliftfun  5843  fliftfund  5844  fliftval  5847  riota5f  5902  f1ofveu  5910  f1ocnvd  6125  f1opw2  6129  off  6148  offval2  6151  ofrfval2  6152  caofref  6159  caofinvl  6160  elxp6  6227  cnvf1olem  6282  f2ndf  6284  f1od2  6293  tposf12  6327  smores2  6352  tfrlemisucaccv  6383  tfrlemibfn  6386  tfr1onlemsucaccv  6399  tfr1onlembfn  6402  tfrcllemsucaccv  6412  tfrcllembfn  6415  tfrcl  6422  tfri3  6425  frecabcl  6457  nnsucsssuc  6550  ersym  6604  ertr  6607  swoer  6620  erth  6638  riinerm  6667  qliftfund  6677  eroprf  6687  ecopoverg  6695  th3qlem1  6696  elmapssres  6732  mapss  6750  fdiagfn  6751  ixpssmap2g  6786  mapsnf1o  6796  f1dom2g  6815  dom3d  6833  pw2f1odclem  6895  fopwdom  6897  mapxpen  6909  nndomo  6925  dif1en  6940  findcard2  6950  findcard2s  6951  diffisn  6954  fimax2gtrilemstep  6961  fientri3  6976  tpfidceq  6991  fiintim  6992  opabfi  6999  f1dmvrnfibi  7010  sbthlemi6  7028  elfir  7039  fifo  7046  supelti  7068  supsnti  7071  cnvinfex  7084  ordiso2  7101  updjud  7148  djudom  7159  difinfsn  7166  ctssdc  7179  enumctlemm  7180  enumct  7181  nninfninc  7189  enomnilem  7204  fodjuf  7211  ismkvnex  7221  omnimkv  7222  enmkvlem  7227  enwomnilem  7235  nninfdcinf  7237  nninfwlporlem  7239  isnumi  7249  exmidfodomrlemrALT  7270  djudoml  7286  djudomr  7287  netap  7321  2omotaplemap  7324  2omotaplemst  7325  exmidapne  7327  cc2lem  7333  cc3  7335  ltsopi  7387  pitri3or  7389  ltdcpi  7390  indpi  7409  enqdc  7428  enqdc1  7429  addcmpblnq  7434  mulcanenq  7452  recrecnq  7461  nqtri3or  7463  ltdcnq  7464  ltsonq  7465  ltaddnq  7474  subhalfnqq  7481  archnqq  7484  prarloclemarch2  7486  enq0tr  7501  nqnq0  7508  addcmpblnq0  7510  mulcanenq0ec  7512  nnnq0lem1  7513  nqpnq0nq  7520  nq0m0r  7523  nq02m  7532  prarloclemlt  7560  prarloclemcalc  7569  addlocpr  7603  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  prmuloclemcalc  7632  mullocprlem  7637  mulnqprlemrl  7640  mulnqprlemru  7641  1idprl  7657  1idpru  7658  ltaddpr  7664  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemdisj  7673  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  addcanprg  7683  prplnqu  7687  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  aptiprleml  7706  aptiprlemu  7707  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlem1  7726  cauappcvgprlem2  7727  caucvgprlemnkj  7733  caucvgprlemopl  7736  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlem2  7747  caucvgprprlemnkltj  7756  caucvgprprlemopl  7764  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlemaddq  7775  caucvgprprlem2  7777  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemloc  7788  suplocexprlemlub  7791  prsrlem1  7809  0idsr  7834  1idsr  7835  recexgt0sr  7840  archsr  7849  prsradd  7853  caucvgsrlemcau  7860  caucvgsrlembound  7861  caucvgsrlemoffgt1  7866  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  pitonnlem1p1  7913  pitonn  7915  pitoregt0  7916  peano2nnnn  7920  recidpirq  7925  axcaucvglemval  7964  leid  8110  nltled  8147  readdcan  8166  addneintrd  8214  addneintr2d  8215  pncan  8232  subsub2  8254  subsub4  8259  negned  8334  subne0d  8346  subneintrd  8381  subneintr2d  8383  subeq0bd  8405  subdi  8411  gt0add  8600  rimul  8612  rereim  8613  ltmul1a  8618  apreim  8630  apirr  8632  mulap0r  8642  msqge0  8643  mulge0  8646  gt0ap0  8653  ltap  8660  subap0d  8671  recexaplem2  8679  mulap0bad  8686  mulap0bbd  8687  mul0eqap  8697  divrecap  8715  div0ap  8729  div1  8730  recrecap  8736  divdivdivap  8740  ddcanap  8753  rerecclap  8757  div2negap  8762  diveqap1bd  8863  recgt0  8877  prodgt0  8879  lemul1a  8885  recp1lt1  8926  squeeze0  8931  peano2nn  9002  div4p1lem1div2  9245  arch  9246  peano2z  9362  peano2zm  9364  ztri3or  9369  nn0n0n1ge2  9396  zextle  9417  gtndiv  9421  suprzclex  9424  nn0ind-raph  9443  uzid  9615  uzneg  9620  uztric  9623  uz11  9624  eluzp1l  9626  qdivcl  9717  irrmul  9721  irrmulap  9722  rpnegap  9761  negelrpd  9763  ledivge1le  9801  mul2lt0rlt0  9834  mul2lt0rgt0  9835  nn0ledivnn  9842  ltpnf  9855  mnflt  9858  pnfge  9864  mnfle  9867  xrlttr  9870  xrltso  9871  xrlttri3  9872  xrleid  9875  xaddass2  9945  xltadd1  9951  xlt2add  9955  xleaddadd  9962  iccf1o  10079  fztri3or  10114  fznlem  10116  fzn  10117  fzsplit2  10125  fznatpl1  10151  uzsplit  10167  fseq1p1m1  10169  fzm1  10175  fznn0sub2  10203  difelfznle  10210  1fv  10214  fzodcel  10228  fzospliti  10252  fzouzsplit  10255  eluzgtdifelfzo  10273  exfzdc  10316  subfzo0  10318  zsupcllemstep  10319  zsupcl  10321  zssinfcl  10322  infssuzex  10323  infssuzcldc  10325  suprzubdc  10326  nninfdcex  10327  qdcle  10336  exbtwnz  10340  qbtwnrelemcalc  10345  flqlelt  10366  qfraclt1  10370  qfracge0  10371  flqltnz  10377  btwnzge0  10390  flhalf  10392  fldiv4lem1div2uz2  10396  ceiqle  10405  intfracq  10412  mulqmod0  10422  modqge0  10424  modqlt  10425  modqid  10441  modqid0  10442  m1modge3gt1  10463  modqltm1p1mod  10468  q2txmodxeq0  10476  modaddmodlo  10480  modsumfzodifsn  10488  addmodlteq  10490  frecuzrdgtcl  10504  frecuzrdgtclt  10513  uzennn  10528  uzsinds  10536  seqf  10556  seqf2  10560  monoord2  10578  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1oleml  10608  seqf1oglem1  10611  ser3le  10629  exp3vallem  10632  exp3val  10633  expp1  10638  expcllem  10642  ltexp2a  10683  leexp2a  10684  nn0ltexp2  10801  faclbnd  10833  faclbnd2  10834  faclbnd3  10835  bcval5  10855  bcpasc  10858  hashennn  10872  fihasheqf1oi  10879  hashsng  10890  fihashfn  10892  hashun  10897  fihashss  10908  fihashssdif  10910  hashfz  10913  hashxp  10918  fimaxq  10919  zfz1isolem1  10932  seq3coll  10934  wrdf  10941  wrdlenge2n0  10970  fstwrdne0  10974  wrdred1hash  10978  shftfn  10989  cjth  11011  cjmulrcl  11052  reim0bd  11109  rerebd  11110  cjrebd  11111  caucvgre  11146  cvg1nlemcxze  11147  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniq  11160  resqrexlemover  11175  resqrexlemdec  11176  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  rersqrtthlem  11195  sqrtgt0  11199  leabs  11239  absexpzap  11245  absle  11254  recvalap  11262  abstri  11269  abs2dif  11271  amgm2  11283  absne0d  11352  maxleim  11370  maxabslemab  11371  maxabslemlub  11372  maxltsup  11383  zmaxcl  11389  fimaxre2  11392  minmax  11395  rpmincl  11403  bdtrilem  11404  bdtri  11405  xrmaxleim  11409  xrmaxiflemcom  11414  xrmaxltsup  11423  xrmaxadd  11426  xrminmax  11430  xrminrpcl  11439  climconst  11455  climuni  11458  2clim  11466  climcn1  11473  climcn2  11474  reccn2ap  11478  climge0  11490  climle  11499  climsqz  11500  climsqz2  11501  serf0  11517  summodclem3  11545  summodclem2a  11546  fsumcl2lem  11563  sumpr  11578  sumtp  11579  fsum0diaglem  11605  mptfzshft  11607  fsumle  11628  fsumlt  11629  divcnv  11662  trireciplem  11665  expcnvap0  11667  expcnv  11669  explecnv  11670  geosergap  11671  cvgratnnlembern  11688  cvgratnnlemabsle  11692  cvgratnnlemsumlt  11693  cvgratz  11697  cvgratgt0  11698  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  clim2divap  11705  prodmodclem3  11740  prodmodclem2a  11741  fprodseq  11748  fprodmul  11756  fprodfac  11780  fprodconst  11785  fprodap0  11786  fprodap0f  11801  fprodle  11805  eftcl  11819  ef0lem  11825  efsub  11846  eftlub  11855  eflegeo  11866  tanval2ap  11878  sinadd  11901  cos2t  11915  cos2tsin  11916  sin01bnd  11922  cos01bnd  11923  eirraplem  11942  dvdsval2  11955  dvdsdc  11963  dvds0lem  11966  zdvdsdc  11977  dvdscmulr  11985  dvdsmulcr  11986  fsumdvds  12007  dvdslelemd  12008  divconjdvds  12014  dvdsext  12020  fzm1ndvds  12021  dvdsmod  12027  3dvds  12029  oexpneg  12042  2tp1odd  12049  mulsucdiv2z  12050  2teven  12052  zeo5  12053  opeo  12062  omeo  12063  nn0ob  12073  divalglemnqt  12085  bits0o  12114  bitsfzolem  12118  bitsfzo  12119  gcddvds  12130  dvdslegcd  12131  gcdneg  12149  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlema  12166  bezoutlemb  12167  bezoutlemmo  12173  bezoutlemle  12175  bezoutlemsup  12176  dfgcd3  12177  bezout  12178  dfgcd2  12181  uzwodc  12204  lcmcllem  12235  lcmneg  12242  lcmgcdlem  12245  lcmdvds  12247  lcmid  12248  3lcm2e6woprm  12254  6lcm4e12  12255  ncoprmgcdne1b  12257  mulgcddvds  12262  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  isprm2lem  12284  prmind2  12288  dvdsnprmd  12293  prm2orodd  12294  sqnprm  12304  isprm5lem  12309  rpexp  12321  sqrt2irrlem  12329  oddpwdclemdc  12341  sqrt2irraplemnn  12347  qnumdencoprm  12361  qeqnumdivden  12362  nn0gcdsq  12368  nn0sqrtelqelz  12374  nonsq  12375  phicl2  12382  phibnd  12385  hashdvds  12389  phiprmpw  12390  phimullem  12393  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemth  12400  prmdiveq  12404  hashgcdlem  12406  odzdvds  12414  modprminv  12418  nnnn0modprm0  12424  modprmn0modprm0  12425  pythagtriplem10  12438  pythagtriplem19  12451  pythagtrip  12452  pcpre1  12461  pcpremul  12462  pceu  12464  pcmul  12470  pcdiv  12471  pcqmul  12472  pcqdiv  12476  pcexp  12478  pcdvdsb  12489  pcidlem  12492  pcdvdstr  12496  pcgcd1  12497  pc2dvds  12499  pcprmpw2  12502  difsqpwdvds  12507  pcaddlem  12508  pcadd  12509  pcadd2  12510  pcmpt  12512  pcmptdvds  12514  pcprod  12515  fldivp1  12517  pcfaclem  12518  pcfac  12519  pcbc  12520  qexpz  12521  pockthlem  12525  pockthg  12526  1arithlem4  12535  1arith  12536  1arith2  12537  4sqlem6  12552  4sqlem8  12554  4sqlem9  12555  4sqlem10  12556  4sqexercise1  12567  4sqexercise2  12568  4sqlemsdc  12569  4sqlem11  12570  4sqlem12  12571  4sqlem15  12574  4sqlem16  12575  4sqlem17  12576  znnen  12615  ennnfonelemk  12617  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemrnh  12633  ennnfonelemfun  12634  ennnfonelemf1  12635  ennnfonelemrn  12636  ennnfonelemnn0  12639  ctinfomlemom  12644  ctiunctlemudc  12654  unct  12659  omctfn  12660  ssnnctlemct  12663  nninfdclemp1  12667  nninfdc  12670  structfung  12695  setsfun  12713  setsfun0  12714  setscom  12718  setsslid  12729  imasaddfnlemg  12957  imasaddvallemg  12958  mgmsscl  13004  plusffng  13008  mgmplusf  13009  mgm0  13012  mgm1  13013  opifismgmdc  13014  gsumfzval  13034  gsumprval  13042  sgrp1  13054  issgrpd  13055  mndpfo  13079  mndfo  13080  mnd1  13087  0subm  13116  mhmima  13123  grpinvfng  13176  isgrpinv  13186  grpinvid  13192  grpinvf1o  13202  grpinvadd  13210  grpsubf  13211  grpsubsub4  13225  grplactcnv  13234  grp1  13238  grp1inv  13239  qusgrp2  13243  mulgfng  13254  subginv  13311  resgrpisgrp  13325  subgintm  13328  0subg  13329  0nsg  13344  qusinv  13366  ghminv  13380  ghmrn  13387  ghmeql  13397  ghmnsgima  13398  kerf1ghm  13404  conjnmz  13409  rngass  13495  rngmneg1  13503  rngmneg2  13504  qusrng  13514  srgideu  13528  srgidmlem  13534  srgpcomp  13546  srg1expzeq1  13551  ringcl  13569  ringideu  13573  ringidmlem  13578  ringnegl  13607  ringnegr  13608  ring1  13615  qusring2  13622  opprringbg  13636  dvdsrd  13650  dvdsr01  13660  isunitd  13662  unitinvcl  13679  unitinvinv  13680  unitnegcl  13686  rhmmul  13720  rhmf1o  13724  nzrunit  13744  lringuplu  13752  subrngintm  13768  subrgsubm  13790  subrgintm  13799  aprsym  13840  scaffng  13865  lmodscaf  13866  lsssn0  13926  lss1d  13939  lssintclm  13940  lspval  13946  lspcl  13947  lspsnid  13963  lspprid1  13967  lspsn  13972  sraval  13993  rspcl  14047  rspssid  14048  rspssp  14050  rnglidlmmgm  14052  rnglidlmsgrp  14053  cnfldneg  14129  zringinvg  14160  expghmap  14163  znzrhfo  14204  znf1o  14207  znhash  14212  znidomb  14214  znrrg  14216  psraddcl  14232  baspartn  14286  eltg3i  14292  tgclb  14301  topbas  14303  2basgeng  14318  topcld  14345  0cld  14348  uncld  14349  neif  14377  elnei  14388  0nei  14402  restbasg  14404  iscnp4  14454  cnpnei  14455  cnclima  14459  cncnp  14466  cnrest2r  14473  cndis  14477  lmff  14485  lmtopcnp  14486  txbas  14494  txopn  14501  txcnp  14507  upxp  14508  txdis1cn  14514  cnmpt11  14519  cnmpt21  14527  psmetge0  14567  xmetge0  14601  xmettpos  14606  xmetrtri  14612  metrtri  14613  xblpnfps  14634  xblpnf  14635  blfps  14645  blf  14646  ssblps  14661  ssbl  14662  blbas  14669  metss2  14734  xmettxlem  14745  xmettx  14746  qtopbas  14758  divcnap  14801  cncfss  14819  cdivcncfap  14840  expcncf  14845  cnopnap  14847  maxcncf  14851  mincncf  14852  dedekindeulemuub  14853  dedekindeulemlu  14857  dedekindeu  14859  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemlu  14866  dedekindicclemicc  14868  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthinc  14879  ivthreinc  14881  hoverlt1  14885  ellimc3apf  14896  limcimolemlt  14900  limcimo  14901  limcresi  14902  cnplimclemle  14904  reldvg  14915  dvfgg  14924  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcjbr  14944  dvcj  14945  dvrecap  14949  dveflem  14962  dvef  14963  elply2  14971  elplyr  14976  plycj  14997  plyreres  15000  reeff1oleme  15008  pilem3  15019  sinq34lt0t  15067  cosq14gt0  15068  coseq0q4123  15070  tangtx  15074  sincosq1eq  15075  cosordlem  15085  logdivlti  15117  relogbval  15187  relogbzcl  15188  nnlogbexp  15195  logbgcd1irr  15203  logbgcd1irraplemexp  15204  logbgcd1irraplemap  15205  wilthlem1  15216  mpodvdsmulf1o  15226  mersenne  15233  perfectlem2  15236  perfect  15237  zabsle1  15240  lgslem1  15241  lgsval  15245  lgsfvalg  15246  lgsfcl2  15247  lgsval2lem  15251  lgscl1  15264  lgsmod  15267  lgsdir2lem5  15273  lgsdir2  15274  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  gausslemma2dlem0c  15292  gausslemma2dlem0h  15297  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem3  15304  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad3  15325  2lgslem3b1  15339  2lgslem3c1  15340  2lgs  15345  2lgsoddprmlem2  15347  2lgsoddprm  15354  2sqlem3  15358  2sqlem8  15364  2sqlem10  15366  fnmptd  15450  bj-sels  15560  bj-nnelon  15605  pwle2  15643  pwf1oexmid  15644  pw1nct  15647  nninfall  15653  nninfsellemdc  15654  nninfself  15657  refeq  15672  isomninnlem  15674  cvgcmp2nlemabs  15676  trilpolemlt1  15685  trirec0  15688  apdifflemf  15690  apdifflemr  15691  apdiff  15692  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  reap0  15702  cndcap  15703