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  2266  eqnetrd  2384  3netr4d  2393  r19.30dc  2637  sbcne12g  3090  eqsstrd  3206  3sstr4d  3215  eqbrtrd  4040  3brtr4d  4050  snelpwi  4230  prelpwi  4232  pwel  4236  ordelon  4401  onin  4404  elelsuc  4427  onsuc  4518  onsucb  4520  onintonm  4534  omsinds  4639  sosng  4717  relssdv  4736  eqbrrdv  4741  eqrelrdv2  4743  relsnopg  4748  breldmg  4851  elrnmptdv  4899  iss  4971  xpimasn  5095  elxp4  5134  elxp5  5135  iotam  5227  funssres  5277  f0rn0  5429  sefvex  5555  fvun1  5603  eqfnfvd  5637  fvimacnvi  5651  fvimacnv  5652  fvelrn  5668  fmpt3d  5693  fmpt2d  5699  resflem  5701  fmptco  5703  fsn  5709  ftpg  5721  fconst2g  5752  funfvima3  5771  elabrexg  5780  foeqcnvco  5812  f1eqcocnv  5813  fliftfun  5818  fliftfund  5819  fliftval  5822  riota5f  5877  f1ofveu  5885  f1ocnvd  6097  f1opw2  6101  off  6120  offval2  6123  ofrfval2  6124  caofref  6129  caofinvl  6130  elxp6  6195  cnvf1olem  6250  f2ndf  6252  f1od2  6261  tposf12  6295  smores2  6320  tfrlemisucaccv  6351  tfrlemibfn  6354  tfr1onlemsucaccv  6367  tfr1onlembfn  6370  tfrcllemsucaccv  6380  tfrcllembfn  6383  tfrcl  6390  tfri3  6393  frecabcl  6425  nnsucsssuc  6518  ersym  6572  ertr  6575  swoer  6588  erth  6606  riinerm  6635  qliftfund  6645  eroprf  6655  ecopoverg  6663  th3qlem1  6664  elmapssres  6700  mapss  6718  fdiagfn  6719  ixpssmap2g  6754  mapsnf1o  6764  f1dom2g  6783  dom3d  6801  pw2f1odclem  6863  fopwdom  6865  mapxpen  6877  nndomo  6893  dif1en  6908  findcard2  6918  findcard2s  6919  diffisn  6922  fimax2gtrilemstep  6929  fientri3  6944  fiintim  6958  f1dmvrnfibi  6974  sbthlemi6  6992  elfir  7003  fifo  7010  supelti  7032  supsnti  7035  cnvinfex  7048  ordiso2  7065  updjud  7112  djudom  7123  difinfsn  7130  ctssdc  7143  enumctlemm  7144  enumct  7145  enomnilem  7167  fodjuf  7174  ismkvnex  7184  omnimkv  7185  enmkvlem  7190  enwomnilem  7198  nninfdcinf  7200  nninfwlporlem  7202  isnumi  7212  exmidfodomrlemrALT  7233  djudoml  7249  djudomr  7250  netap  7284  2omotaplemap  7287  2omotaplemst  7288  exmidapne  7290  cc2lem  7296  cc3  7298  ltsopi  7350  pitri3or  7352  ltdcpi  7353  indpi  7372  enqdc  7391  enqdc1  7392  addcmpblnq  7397  mulcanenq  7415  recrecnq  7424  nqtri3or  7426  ltdcnq  7427  ltsonq  7428  ltaddnq  7437  subhalfnqq  7444  archnqq  7447  prarloclemarch2  7449  enq0tr  7464  nqnq0  7471  addcmpblnq0  7473  mulcanenq0ec  7475  nnnq0lem1  7476  nqpnq0nq  7483  nq0m0r  7486  nq02m  7495  prarloclemlt  7523  prarloclemcalc  7532  addlocpr  7566  nqprl  7581  nqpru  7582  addnqprlemrl  7587  addnqprlemru  7588  prmuloclemcalc  7595  mullocprlem  7600  mulnqprlemrl  7603  mulnqprlemru  7604  1idprl  7620  1idpru  7621  ltaddpr  7627  ltexprlemm  7630  ltexprlemopl  7631  ltexprlemopu  7633  ltexprlemdisj  7636  ltexprlemrl  7640  ltexprlemru  7642  addcanprleml  7644  addcanprlemu  7645  addcanprg  7646  prplnqu  7650  recexprlemloc  7661  recexprlem1ssl  7663  recexprlem1ssu  7664  aptiprleml  7669  aptiprlemu  7670  archpr  7673  cauappcvgprlemm  7675  cauappcvgprlemopl  7676  cauappcvgprlemloc  7682  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  cauappcvgprlem1  7689  cauappcvgprlem2  7690  caucvgprlemnkj  7696  caucvgprlemopl  7699  caucvgprlemloc  7705  caucvgprlemladdfu  7707  caucvgprlem2  7710  caucvgprprlemnkltj  7719  caucvgprprlemopl  7727  caucvgprprlemloc  7733  caucvgprprlemexbt  7736  caucvgprprlemaddq  7738  caucvgprprlem2  7740  suplocexprlemmu  7748  suplocexprlemru  7749  suplocexprlemloc  7751  suplocexprlemlub  7754  prsrlem1  7772  0idsr  7797  1idsr  7798  recexgt0sr  7803  archsr  7812  prsradd  7816  caucvgsrlemcau  7823  caucvgsrlembound  7824  caucvgsrlemoffgt1  7829  suplocsrlemb  7836  suplocsrlempr  7837  suplocsrlem  7838  pitonnlem1p1  7876  pitonn  7878  pitoregt0  7879  peano2nnnn  7883  recidpirq  7888  axcaucvglemval  7927  leid  8072  nltled  8109  readdcan  8128  addneintrd  8176  addneintr2d  8177  pncan  8194  subsub2  8216  subsub4  8221  negned  8296  subne0d  8308  subneintrd  8343  subneintr2d  8345  subeq0bd  8367  subdi  8373  gt0add  8561  rimul  8573  rereim  8574  ltmul1a  8579  apreim  8591  apirr  8593  mulap0r  8603  msqge0  8604  mulge0  8607  gt0ap0  8614  ltap  8621  subap0d  8632  recexaplem2  8640  mulap0bad  8647  mulap0bbd  8648  mul0eqap  8658  divrecap  8676  div0ap  8690  div1  8691  recrecap  8697  divdivdivap  8701  ddcanap  8714  rerecclap  8718  div2negap  8723  diveqap1bd  8824  recgt0  8838  prodgt0  8840  lemul1a  8846  recp1lt1  8887  squeeze0  8892  peano2nn  8962  div4p1lem1div2  9203  arch  9204  peano2z  9320  peano2zm  9322  ztri3or  9327  nn0n0n1ge2  9354  zextle  9375  gtndiv  9379  suprzclex  9382  nn0ind-raph  9401  uzid  9573  uzneg  9578  uztric  9581  uz11  9582  eluzp1l  9584  qdivcl  9675  irrmul  9679  rpnegap  9718  negelrpd  9720  ledivge1le  9758  mul2lt0rlt0  9791  mul2lt0rgt0  9792  nn0ledivnn  9799  ltpnf  9812  mnflt  9815  pnfge  9821  mnfle  9824  xrlttr  9827  xrltso  9828  xrlttri3  9829  xrleid  9832  xaddass2  9902  xltadd1  9908  xlt2add  9912  xleaddadd  9919  iccf1o  10036  fztri3or  10071  fznlem  10073  fzn  10074  fzsplit2  10082  fznatpl1  10108  uzsplit  10124  fseq1p1m1  10126  fzm1  10132  fznn0sub2  10160  difelfznle  10167  1fv  10171  fzodcel  10184  fzospliti  10208  fzouzsplit  10211  eluzgtdifelfzo  10229  exfzdc  10272  subfzo0  10274  exbtwnz  10283  qbtwnrelemcalc  10288  flqlelt  10309  qfraclt1  10313  qfracge0  10314  flqltnz  10320  btwnzge0  10333  flhalf  10335  ceiqle  10346  intfracq  10353  mulqmod0  10363  modqge0  10365  modqlt  10366  modqid  10382  modqid0  10383  m1modge3gt1  10404  modqltm1p1mod  10409  q2txmodxeq0  10417  modaddmodlo  10421  modsumfzodifsn  10429  addmodlteq  10431  frecuzrdgtcl  10445  frecuzrdgtclt  10454  uzennn  10469  uzsinds  10475  seqf  10494  seqf2  10497  monoord2  10510  iseqf1olemqk  10527  iseqf1olemjpcl  10528  iseqf1olemqpcl  10529  seq3f1olemqsumkj  10531  seq3f1olemqsum  10533  seq3f1olemstep  10534  seq3f1oleml  10536  ser3le  10552  exp3vallem  10555  exp3val  10556  expp1  10561  expcllem  10565  ltexp2a  10606  leexp2a  10607  nn0ltexp2  10724  faclbnd  10756  faclbnd2  10757  faclbnd3  10758  bcval5  10778  bcpasc  10781  hashennn  10795  fihasheqf1oi  10802  hashsng  10813  fihashfn  10815  hashun  10820  fihashss  10831  fihashssdif  10833  hashfz  10836  hashxp  10841  fimaxq  10842  zfz1isolem1  10855  seq3coll  10857  shftfn  10868  cjth  10890  cjmulrcl  10931  reim0bd  10988  rerebd  10989  cjrebd  10990  caucvgre  11025  cvg1nlemcxze  11026  cvg1nlemcau  11028  cvg1nlemres  11029  recvguniq  11039  resqrexlemover  11054  resqrexlemdec  11055  resqrexlemgt0  11064  resqrexlemoverl  11065  resqrexlemglsq  11066  rersqrtthlem  11074  sqrtgt0  11078  leabs  11118  absexpzap  11124  absle  11133  recvalap  11141  abstri  11148  abs2dif  11150  amgm2  11162  absne0d  11231  maxleim  11249  maxabslemab  11250  maxabslemlub  11251  maxltsup  11262  zmaxcl  11268  fimaxre2  11270  minmax  11273  rpmincl  11281  bdtrilem  11282  bdtri  11283  xrmaxleim  11287  xrmaxiflemcom  11292  xrmaxltsup  11301  xrmaxadd  11304  xrminmax  11308  xrminrpcl  11317  climconst  11333  climuni  11336  2clim  11344  climcn1  11351  climcn2  11352  reccn2ap  11356  climge0  11368  climle  11377  climsqz  11378  climsqz2  11379  serf0  11395  summodclem3  11423  summodclem2a  11424  fsumcl2lem  11441  sumpr  11456  sumtp  11457  fsum0diaglem  11483  mptfzshft  11485  fsumle  11506  fsumlt  11507  divcnv  11540  trireciplem  11543  expcnvap0  11545  expcnv  11547  explecnv  11548  geosergap  11549  cvgratnnlembern  11566  cvgratnnlemabsle  11570  cvgratnnlemsumlt  11571  cvgratz  11575  cvgratgt0  11576  mertenslemi1  11578  mertenslem2  11579  mertensabs  11580  clim2divap  11583  prodmodclem3  11618  prodmodclem2a  11619  fprodseq  11626  fprodmul  11634  fprodfac  11658  fprodconst  11663  fprodap0  11664  fprodap0f  11679  fprodle  11683  eftcl  11697  ef0lem  11703  efsub  11724  eftlub  11733  eflegeo  11744  tanval2ap  11756  sinadd  11779  cos2t  11793  cos2tsin  11794  sin01bnd  11800  cos01bnd  11801  eirraplem  11819  dvdsval2  11832  dvdsdc  11840  dvds0lem  11843  zdvdsdc  11854  dvdscmulr  11862  dvdsmulcr  11863  dvdslelemd  11884  divconjdvds  11890  dvdsext  11896  fzm1ndvds  11897  dvdsmod  11903  oexpneg  11917  2tp1odd  11924  mulsucdiv2z  11925  2teven  11927  zeo5  11928  opeo  11937  omeo  11938  nn0ob  11948  divalglemnqt  11960  zsupcllemstep  11981  zsupcl  11983  zssinfcl  11984  infssuzex  11985  infssuzcldc  11987  suprzubdc  11988  nninfdcex  11989  gcddvds  11999  dvdslegcd  12000  gcdneg  12018  bezoutlemnewy  12032  bezoutlemstep  12033  bezoutlema  12035  bezoutlemb  12036  bezoutlemmo  12042  bezoutlemle  12044  bezoutlemsup  12045  dfgcd3  12046  bezout  12047  dfgcd2  12050  uzwodc  12073  lcmcllem  12102  lcmneg  12109  lcmgcdlem  12112  lcmdvds  12114  lcmid  12115  3lcm2e6woprm  12121  6lcm4e12  12122  ncoprmgcdne1b  12124  mulgcddvds  12129  divgcdcoprmex  12137  cncongr1  12138  cncongr2  12139  isprm2lem  12151  prmind2  12155  dvdsnprmd  12160  prm2orodd  12161  sqnprm  12171  isprm5lem  12176  rpexp  12188  sqrt2irrlem  12196  oddpwdclemdc  12208  sqrt2irraplemnn  12214  qnumdencoprm  12228  qeqnumdivden  12229  nn0gcdsq  12235  nn0sqrtelqelz  12241  nonsq  12242  phicl2  12249  phibnd  12252  hashdvds  12256  phiprmpw  12257  phimullem  12260  eulerthlemrprm  12264  eulerthlema  12265  eulerthlemth  12267  prmdiveq  12271  hashgcdlem  12273  odzdvds  12280  modprminv  12284  nnnn0modprm0  12290  modprmn0modprm0  12291  pythagtriplem10  12304  pythagtriplem19  12317  pythagtrip  12318  pcpre1  12327  pcpremul  12328  pceu  12330  pcmul  12336  pcdiv  12337  pcqmul  12338  pcqdiv  12342  pcexp  12344  pcdvdsb  12355  pcidlem  12358  pcdvdstr  12362  pcgcd1  12363  pc2dvds  12365  pcprmpw2  12368  difsqpwdvds  12373  pcaddlem  12374  pcadd  12375  pcadd2  12376  pcmpt  12378  pcmptdvds  12380  pcprod  12381  fldivp1  12383  pcfaclem  12384  pcfac  12385  pcbc  12386  qexpz  12387  pockthlem  12391  pockthg  12392  1arithlem4  12401  1arith  12402  1arith2  12403  4sqlem6  12418  4sqlem8  12420  4sqlem9  12421  4sqlem10  12422  4sqexercise1  12433  4sqexercise2  12434  4sqlemsdc  12435  4sqlem11  12436  4sqlem12  12437  4sqlem15  12440  4sqlem16  12441  4sqlem17  12442  znnen  12452  ennnfonelemk  12454  ennnfonelemkh  12466  ennnfonelemhf1o  12467  ennnfonelemrnh  12470  ennnfonelemfun  12471  ennnfonelemf1  12472  ennnfonelemrn  12473  ennnfonelemnn0  12476  ctinfomlemom  12481  ctiunctlemudc  12491  unct  12496  omctfn  12497  ssnnctlemct  12500  nninfdclemp1  12504  nninfdc  12507  structfung  12532  setsfun  12550  setsfun0  12551  setscom  12555  setsslid  12566  imasaddfnlemg  12794  imasaddvallemg  12795  mgmsscl  12840  plusffng  12844  mgmplusf  12845  mgm0  12848  mgm1  12849  opifismgmdc  12850  gsumprval  12877  sgrp1  12889  issgrpd  12890  mndpfo  12914  mndfo  12915  mnd1  12922  0subm  12951  mhmima  12958  grpinvfng  13003  isgrpinv  13013  grpinvid  13019  grpinvf1o  13029  grpinvadd  13037  grpsubf  13038  grpsubsub4  13052  grplactcnv  13061  grp1  13065  grp1inv  13066  qusgrp2  13070  mulgfng  13081  subginv  13137  resgrpisgrp  13151  subgintm  13154  0subg  13155  0nsg  13170  qusinv  13192  ghminv  13206  ghmrn  13213  ghmeql  13223  ghmnsgima  13224  kerf1ghm  13230  conjnmz  13235  rngass  13310  rngmneg1  13318  rngmneg2  13319  qusrng  13329  srgideu  13343  srgidmlem  13349  srgpcomp  13361  srg1expzeq1  13366  ringcl  13384  ringideu  13388  ringidmlem  13393  ringnegl  13420  ringnegr  13421  ring1  13428  qusring2  13433  opprringbg  13447  dvdsrd  13461  dvdsr01  13471  isunitd  13473  unitinvcl  13490  unitinvinv  13491  unitnegcl  13497  rhmmul  13531  rhmf1o  13535  nzrunit  13552  lringuplu  13560  subrngintm  13576  subrgsubm  13598  subrgintm  13607  aprsym  13617  scaffng  13642  lmodscaf  13643  lsssn0  13703  lss1d  13716  lssintclm  13717  lspval  13723  lspcl  13724  lspsnid  13740  lspprid1  13744  lspsn  13749  sraval  13770  rspcl  13824  rspssid  13825  rspssp  13827  rnglidlmmgm  13829  rnglidlmsgrp  13830  cnfldneg  13893  zringinvg  13920  psraddcl  13973  baspartn  14027  eltg3i  14033  tgclb  14042  topbas  14044  2basgeng  14059  topcld  14086  0cld  14089  uncld  14090  neif  14118  elnei  14129  0nei  14143  restbasg  14145  iscnp4  14195  cnpnei  14196  cnclima  14200  cncnp  14207  cnrest2r  14214  cndis  14218  lmff  14226  lmtopcnp  14227  txbas  14235  txopn  14242  txcnp  14248  upxp  14249  txdis1cn  14255  cnmpt11  14260  cnmpt21  14268  psmetge0  14308  xmetge0  14342  xmettpos  14347  xmetrtri  14353  metrtri  14354  xblpnfps  14375  xblpnf  14376  blfps  14386  blf  14387  ssblps  14402  ssbl  14403  blbas  14410  metss2  14475  xmettxlem  14486  xmettx  14487  qtopbas  14499  divcnap  14532  cncfss  14547  cdivcncfap  14564  expcncf  14569  cnopnap  14571  dedekindeulemuub  14572  dedekindeulemlu  14576  dedekindeu  14578  suplociccex  14580  dedekindicclemuub  14581  dedekindicclemlu  14585  dedekindicclemicc  14587  ivthinclemlopn  14591  ivthinclemuopn  14593  ivthinc  14598  ellimc3apf  14606  limcimolemlt  14610  limcimo  14611  limcresi  14612  cnplimclemle  14614  reldvg  14625  dvfgg  14634  dvidlemap  14637  dvcjbr  14649  dvcj  14650  dvrecap  14654  dveflem  14664  dvef  14665  reeff1oleme  14670  pilem3  14681  sinq34lt0t  14729  cosq14gt0  14730  coseq0q4123  14732  tangtx  14736  sincosq1eq  14737  cosordlem  14747  logdivlti  14779  relogbval  14846  relogbzcl  14847  nnlogbexp  14854  logbgcd1irr  14862  logbgcd1irraplemexp  14863  logbgcd1irraplemap  14864  wilthlem1  14875  zabsle1  14878  lgslem1  14879  lgsval  14883  lgsfvalg  14884  lgsfcl2  14885  lgsval2lem  14889  lgscl1  14902  lgsmod  14905  lgsdir2lem5  14911  lgsdir2  14912  lgsdilem2  14915  lgsdi  14916  lgsne0  14917  lgseisenlem1  14928  lgseisenlem2  14929  2lgsoddprmlem2  14932  2sqlem3  14942  2sqlem8  14948  2sqlem10  14950  fnmptd  15034  bj-sels  15144  bj-nnelon  15189  pwle2  15227  pwf1oexmid  15228  pw1nct  15231  nninfall  15237  nninfsellemdc  15238  nninfself  15241  refeq  15255  isomninnlem  15257  cvgcmp2nlemabs  15259  trilpolemlt1  15268  trirec0  15271  apdifflemf  15273  apdifflemr  15274  apdiff  15275  iswomninnlem  15276  iswomni0  15278  ismkvnnlem  15279  reap0  15285  cndcap  15286