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  706  mpbir2and  944  pm3.12dc  958  mpbir3and  1180  pm5.15dc  1389  eqeltrd  2252  eqnetrd  2369  3netr4d  2378  r19.30dc  2622  sbcne12g  3073  eqsstrd  3189  3sstr4d  3198  eqbrtrd  4020  3brtr4d  4030  snelpwi  4206  prelpwi  4208  pwel  4212  ordelon  4377  onin  4380  elelsuc  4403  suceloni  4494  sucelon  4496  onintonm  4510  omsinds  4615  sosng  4693  relssdv  4712  eqbrrdv  4717  eqrelrdv2  4719  relsnopg  4724  breldmg  4826  elrnmptdv  4874  iss  4946  xpimasn  5069  elxp4  5108  elxp5  5109  iotam  5200  funssres  5250  f0rn0  5402  sefvex  5528  fvun1  5574  eqfnfvd  5608  fvimacnvi  5622  fvimacnv  5623  fvelrn  5639  fmpt3d  5664  fmpt2d  5670  resflem  5672  fmptco  5674  fsn  5680  ftpg  5692  fconst2g  5723  funfvima3  5741  foeqcnvco  5781  f1eqcocnv  5782  fliftfun  5787  fliftfund  5788  fliftval  5791  riota5f  5845  f1ofveu  5853  f1ocnvd  6063  f1opw2  6067  off  6085  offval2  6088  ofrfval2  6089  caofref  6094  caofinvl  6095  elxp6  6160  cnvf1olem  6215  f2ndf  6217  f1od2  6226  tposf12  6260  smores2  6285  tfrlemisucaccv  6316  tfrlemibfn  6319  tfr1onlemsucaccv  6332  tfr1onlembfn  6335  tfrcllemsucaccv  6345  tfrcllembfn  6348  tfrcl  6355  tfri3  6358  frecabcl  6390  nnsucsssuc  6483  ersym  6537  ertr  6540  swoer  6553  erth  6569  riinerm  6598  qliftfund  6608  eroprf  6618  ecopoverg  6626  th3qlem1  6627  elmapssres  6663  mapss  6681  fdiagfn  6682  ixpssmap2g  6717  mapsnf1o  6727  f1dom2g  6746  dom3d  6764  fopwdom  6826  mapxpen  6838  nndomo  6854  dif1en  6869  findcard2  6879  findcard2s  6880  diffisn  6883  fimax2gtrilemstep  6890  fientri3  6904  fiintim  6918  f1dmvrnfibi  6933  sbthlemi6  6951  elfir  6962  fifo  6969  supelti  6991  supsnti  6994  cnvinfex  7007  ordiso2  7024  updjud  7071  djudom  7082  difinfsn  7089  ctssdc  7102  enumctlemm  7103  enumct  7104  enomnilem  7126  fodjuf  7133  ismkvnex  7143  omnimkv  7144  enmkvlem  7149  enwomnilem  7157  nninfdcinf  7159  nninfwlporlem  7161  isnumi  7171  exmidfodomrlemrALT  7192  djudoml  7208  djudomr  7209  cc2lem  7240  cc3  7242  ltsopi  7294  pitri3or  7296  ltdcpi  7297  indpi  7316  enqdc  7335  enqdc1  7336  addcmpblnq  7341  mulcanenq  7359  recrecnq  7368  nqtri3or  7370  ltdcnq  7371  ltsonq  7372  ltaddnq  7381  subhalfnqq  7388  archnqq  7391  prarloclemarch2  7393  enq0tr  7408  nqnq0  7415  addcmpblnq0  7417  mulcanenq0ec  7419  nnnq0lem1  7420  nqpnq0nq  7427  nq0m0r  7430  nq02m  7439  prarloclemlt  7467  prarloclemcalc  7476  addlocpr  7510  nqprl  7525  nqpru  7526  addnqprlemrl  7531  addnqprlemru  7532  prmuloclemcalc  7539  mullocprlem  7544  mulnqprlemrl  7547  mulnqprlemru  7548  1idprl  7564  1idpru  7565  ltaddpr  7571  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemdisj  7580  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  addcanprg  7590  prplnqu  7594  recexprlemloc  7605  recexprlem1ssl  7607  recexprlem1ssu  7608  aptiprleml  7613  aptiprlemu  7614  archpr  7617  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemloc  7626  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlem1  7633  cauappcvgprlem2  7634  caucvgprlemnkj  7640  caucvgprlemopl  7643  caucvgprlemloc  7649  caucvgprlemladdfu  7651  caucvgprlem2  7654  caucvgprprlemnkltj  7663  caucvgprprlemopl  7671  caucvgprprlemloc  7677  caucvgprprlemexbt  7680  caucvgprprlemaddq  7682  caucvgprprlem2  7684  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemloc  7695  suplocexprlemlub  7698  prsrlem1  7716  0idsr  7741  1idsr  7742  recexgt0sr  7747  archsr  7756  prsradd  7760  caucvgsrlemcau  7767  caucvgsrlembound  7768  caucvgsrlemoffgt1  7773  suplocsrlemb  7780  suplocsrlempr  7781  suplocsrlem  7782  pitonnlem1p1  7820  pitonn  7822  pitoregt0  7823  peano2nnnn  7827  recidpirq  7832  axcaucvglemval  7871  leid  8015  nltled  8052  readdcan  8071  addneintrd  8119  addneintr2d  8120  pncan  8137  subsub2  8159  subsub4  8164  negned  8239  subne0d  8251  subneintrd  8286  subneintr2d  8288  subeq0bd  8310  subdi  8316  gt0add  8504  rimul  8516  rereim  8517  ltmul1a  8522  apreim  8534  apirr  8536  mulap0r  8546  msqge0  8547  mulge0  8550  gt0ap0  8557  ltap  8564  subap0d  8575  recexaplem2  8582  mulap0bad  8589  mulap0bbd  8590  mul0eqap  8600  divrecap  8618  div0ap  8632  div1  8633  recrecap  8639  divdivdivap  8643  ddcanap  8656  rerecclap  8660  div2negap  8665  diveqap1bd  8766  recgt0  8780  prodgt0  8782  lemul1a  8788  recp1lt1  8829  squeeze0  8834  peano2nn  8904  div4p1lem1div2  9145  arch  9146  peano2z  9262  peano2zm  9264  ztri3or  9269  nn0n0n1ge2  9296  zextle  9317  gtndiv  9321  suprzclex  9324  nn0ind-raph  9343  uzid  9515  uzneg  9519  uztric  9522  uz11  9523  eluzp1l  9525  qdivcl  9616  irrmul  9620  rpnegap  9657  negelrpd  9659  ledivge1le  9697  mul2lt0rlt0  9730  mul2lt0rgt0  9731  nn0ledivnn  9738  ltpnf  9751  mnflt  9754  pnfge  9760  mnfle  9763  xrlttr  9766  xrltso  9767  xrlttri3  9768  xrleid  9771  xaddass2  9841  xltadd1  9847  xlt2add  9851  xleaddadd  9858  iccf1o  9975  fztri3or  10009  fznlem  10011  fzn  10012  fzsplit2  10020  fznatpl1  10046  uzsplit  10062  fseq1p1m1  10064  fzm1  10070  fznn0sub2  10098  difelfznle  10105  1fv  10109  fzodcel  10122  fzospliti  10146  fzouzsplit  10149  eluzgtdifelfzo  10167  exfzdc  10210  subfzo0  10212  exbtwnz  10221  qbtwnrelemcalc  10226  flqlelt  10246  qfraclt1  10250  qfracge0  10251  flqltnz  10257  btwnzge0  10270  flhalf  10272  ceiqle  10283  intfracq  10290  mulqmod0  10300  modqge0  10302  modqlt  10303  modqid  10319  modqid0  10320  m1modge3gt1  10341  modqltm1p1mod  10346  q2txmodxeq0  10354  modaddmodlo  10358  modsumfzodifsn  10366  addmodlteq  10368  frecuzrdgtcl  10382  frecuzrdgtclt  10391  uzennn  10406  uzsinds  10412  seqf  10431  seqf2  10434  monoord2  10447  iseqf1olemqk  10464  iseqf1olemjpcl  10465  iseqf1olemqpcl  10466  seq3f1olemqsumkj  10468  seq3f1olemqsum  10470  seq3f1olemstep  10471  seq3f1oleml  10473  ser3le  10488  exp3vallem  10491  exp3val  10492  expp1  10497  expcllem  10501  ltexp2a  10542  leexp2a  10543  nn0ltexp2  10658  faclbnd  10689  faclbnd2  10690  faclbnd3  10691  bcval5  10711  bcpasc  10714  hashennn  10728  fihasheqf1oi  10735  hashsng  10746  fihashfn  10748  hashun  10753  fihashss  10764  fihashssdif  10766  hashfz  10769  hashxp  10774  fimaxq  10775  zfz1isolem1  10788  seq3coll  10790  shftfn  10801  cjth  10823  cjmulrcl  10864  reim0bd  10921  rerebd  10922  cjrebd  10923  caucvgre  10958  cvg1nlemcxze  10959  cvg1nlemcau  10961  cvg1nlemres  10962  recvguniq  10972  resqrexlemover  10987  resqrexlemdec  10988  resqrexlemgt0  10997  resqrexlemoverl  10998  resqrexlemglsq  10999  rersqrtthlem  11007  sqrtgt0  11011  leabs  11051  absexpzap  11057  absle  11066  recvalap  11074  abstri  11081  abs2dif  11083  amgm2  11095  absne0d  11164  maxleim  11182  maxabslemab  11183  maxabslemlub  11184  maxltsup  11195  zmaxcl  11201  fimaxre2  11203  minmax  11206  rpmincl  11214  bdtrilem  11215  bdtri  11216  xrmaxleim  11220  xrmaxiflemcom  11225  xrmaxltsup  11234  xrmaxadd  11237  xrminmax  11241  xrminrpcl  11250  climconst  11266  climuni  11269  2clim  11277  climcn1  11284  climcn2  11285  reccn2ap  11289  climge0  11301  climle  11310  climsqz  11311  climsqz2  11312  serf0  11328  summodclem3  11356  summodclem2a  11357  fsumcl2lem  11374  sumpr  11389  sumtp  11390  fsum0diaglem  11416  mptfzshft  11418  fsumle  11439  fsumlt  11440  divcnv  11473  trireciplem  11476  expcnvap0  11478  expcnv  11480  explecnv  11481  geosergap  11482  cvgratnnlembern  11499  cvgratnnlemabsle  11503  cvgratnnlemsumlt  11504  cvgratz  11508  cvgratgt0  11509  mertenslemi1  11511  mertenslem2  11512  mertensabs  11513  clim2divap  11516  prodmodclem3  11551  prodmodclem2a  11552  fprodseq  11559  fprodmul  11567  fprodfac  11591  fprodconst  11596  fprodap0  11597  fprodap0f  11612  fprodle  11616  eftcl  11630  ef0lem  11636  efsub  11657  eftlub  11666  eflegeo  11677  tanval2ap  11689  sinadd  11712  cos2t  11726  cos2tsin  11727  sin01bnd  11733  cos01bnd  11734  eirraplem  11752  dvdsval2  11765  dvdsdc  11773  dvds0lem  11776  zdvdsdc  11787  dvdscmulr  11795  dvdsmulcr  11796  dvdslelemd  11816  divconjdvds  11822  dvdsext  11828  fzm1ndvds  11829  dvdsmod  11835  oexpneg  11849  2tp1odd  11856  mulsucdiv2z  11857  2teven  11859  zeo5  11860  opeo  11869  omeo  11870  nn0ob  11880  divalglemnqt  11892  zsupcllemstep  11913  zsupcl  11915  zssinfcl  11916  infssuzex  11917  infssuzcldc  11919  suprzubdc  11920  nninfdcex  11921  gcddvds  11931  dvdslegcd  11932  gcdneg  11950  bezoutlemnewy  11964  bezoutlemstep  11965  bezoutlema  11967  bezoutlemb  11968  bezoutlemmo  11974  bezoutlemle  11976  bezoutlemsup  11977  dfgcd3  11978  bezout  11979  dfgcd2  11982  uzwodc  12005  lcmcllem  12034  lcmneg  12041  lcmgcdlem  12044  lcmdvds  12046  lcmid  12047  3lcm2e6woprm  12053  6lcm4e12  12054  ncoprmgcdne1b  12056  mulgcddvds  12061  divgcdcoprmex  12069  cncongr1  12070  cncongr2  12071  isprm2lem  12083  prmind2  12087  dvdsnprmd  12092  prm2orodd  12093  sqnprm  12103  isprm5lem  12108  rpexp  12120  sqrt2irrlem  12128  oddpwdclemdc  12140  sqrt2irraplemnn  12146  qnumdencoprm  12160  qeqnumdivden  12161  nn0gcdsq  12167  nn0sqrtelqelz  12173  nonsq  12174  phicl2  12181  phibnd  12184  hashdvds  12188  phiprmpw  12189  phimullem  12192  eulerthlemrprm  12196  eulerthlema  12197  eulerthlemth  12199  prmdiveq  12203  hashgcdlem  12205  odzdvds  12212  modprminv  12216  nnnn0modprm0  12222  modprmn0modprm0  12223  pythagtriplem10  12236  pythagtriplem19  12249  pythagtrip  12250  pcpre1  12259  pcpremul  12260  pceu  12262  pcmul  12268  pcdiv  12269  pcqmul  12270  pcqdiv  12274  pcexp  12276  pcdvdsb  12286  pcidlem  12289  pcdvdstr  12293  pcgcd1  12294  pc2dvds  12296  pcprmpw2  12299  difsqpwdvds  12304  pcaddlem  12305  pcadd  12306  pcmpt  12308  pcmptdvds  12310  pcprod  12311  fldivp1  12313  pcfaclem  12314  pcfac  12315  pcbc  12316  qexpz  12317  pockthlem  12321  pockthg  12322  1arithlem4  12331  1arith  12332  1arith2  12333  4sqlem6  12348  4sqlem8  12350  4sqlem9  12351  4sqlem10  12352  znnen  12366  ennnfonelemk  12368  ennnfonelemkh  12380  ennnfonelemhf1o  12381  ennnfonelemrnh  12384  ennnfonelemfun  12385  ennnfonelemf1  12386  ennnfonelemrn  12387  ennnfonelemnn0  12390  ctinfomlemom  12395  ctiunctlemudc  12405  unct  12410  omctfn  12411  ssnnctlemct  12414  nninfdclemp1  12418  nninfdc  12421  structfung  12446  setsfun  12464  setsfun0  12465  setscom  12469  setsslid  12479  mgmsscl  12646  plusffng  12650  mgmplusf  12651  mgm0  12654  mgm1  12655  opifismgmdc  12656  sgrp1  12682  mndpfo  12705  mndfo  12706  mnd1  12710  0subm  12733  mhmima  12737  grpinvfng  12779  isgrpinv  12788  grpinvid  12792  grpinvf1o  12801  grpinvadd  12809  grpsubf  12810  grpsubsub4  12824  grplactcnv  12833  grp1  12837  grp1inv  12838  mulgfng  12848  srgideu  12952  srgidmlem  12958  srgpcomp  12970  srg1expzeq1  12975  ringcl  12993  ringideu  12997  ringidmlem  13002  ringnegl  13024  rngnegr  13025  ring1  13032  opprringbg  13045  baspartn  13119  eltg3i  13127  tgclb  13136  topbas  13138  2basgeng  13153  topcld  13180  0cld  13183  uncld  13184  neif  13212  elnei  13223  0nei  13237  restbasg  13239  iscnp4  13289  cnpnei  13290  cnclima  13294  cncnp  13301  cnrest2r  13308  cndis  13312  lmff  13320  lmtopcnp  13321  txbas  13329  txopn  13336  txcnp  13342  upxp  13343  txdis1cn  13349  cnmpt11  13354  cnmpt21  13362  psmetge0  13402  xmetge0  13436  xmettpos  13441  xmetrtri  13447  metrtri  13448  xblpnfps  13469  xblpnf  13470  blfps  13480  blf  13481  ssblps  13496  ssbl  13497  blbas  13504  metss2  13569  xmettxlem  13580  xmettx  13581  qtopbas  13593  divcnap  13626  cncfss  13641  cdivcncfap  13658  expcncf  13663  cnopnap  13665  dedekindeulemuub  13666  dedekindeulemlu  13670  dedekindeu  13672  suplociccex  13674  dedekindicclemuub  13675  dedekindicclemlu  13679  dedekindicclemicc  13681  ivthinclemlopn  13685  ivthinclemuopn  13687  ivthinc  13692  ellimc3apf  13700  limcimolemlt  13704  limcimo  13705  limcresi  13706  cnplimclemle  13708  reldvg  13719  dvfgg  13728  dvidlemap  13731  dvcjbr  13743  dvcj  13744  dvrecap  13748  dveflem  13758  dvef  13759  reeff1oleme  13764  pilem3  13775  sinq34lt0t  13823  cosq14gt0  13824  coseq0q4123  13826  tangtx  13830  sincosq1eq  13831  cosordlem  13841  logdivlti  13873  relogbval  13940  relogbzcl  13941  nnlogbexp  13948  logbgcd1irr  13956  logbgcd1irraplemexp  13957  logbgcd1irraplemap  13958  zabsle1  13971  lgslem1  13972  lgsval  13976  lgsfvalg  13977  lgsfcl2  13978  lgsval2lem  13982  lgscl1  13995  lgsmod  13998  lgsdir2lem5  14004  lgsdir2  14005  lgsdilem2  14008  lgsdi  14009  lgsne0  14010  2sqlem3  14024  2sqlem8  14030  2sqlem10  14032  fnmptd  14116  bj-sels  14226  bj-nnelon  14271  pwle2  14308  pwf1oexmid  14309  pw1nct  14313  nninfall  14319  nninfsellemdc  14320  nninfself  14323  refeq  14337  isomninnlem  14339  cvgcmp2nlemabs  14341  trilpolemlt1  14350  trirec0  14353  apdifflemf  14355  apdifflemr  14356  apdiff  14357  iswomninnlem  14358  iswomni0  14360  ismkvnnlem  14361  reap0  14367