Theorem mpbid 146

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

Hypotheses

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

Assertion

Ref	Expression
mpbid	|- ( ph -> ch )

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 |- ( ph -> ps )
2		mpbid.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 143	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbii  147  annimdc  932  mpbi2and  938  bilukdc  1391  equs5or  1823  eqtrd  2203  eleqtrd  2249  neeqtrd  2368  3netr3d  2372  rexlimd2  2585  ceqsalt  2756  vtoclgft  2780  vtoclegft  2802  elrab3t  2885  eueq2dc  2903  sbceq1dd  2961  csbiedf  3089  sseqtrd  3185  3sstr3d  3191  ifbothdadc  3557  snssd  3725  dfnfc2  3814  breqdi  4004  breqtrd  4015  3brtr3d  4020  csbexga  4117  reuhypd  4456  reg2exmidlema  4518  elirr  4525  en2lp  4538  onsucuni2  4548  finds  4584  iota4  5178  iota4an  5179  funimaexglem  5281  fneu  5302  fco2  5364  fssres2  5375  fresin  5376  feu  5380  f1orescnv  5458  resdif  5464  funcocnv2  5467  f1oprg  5486  fvelrnb  5544  fimacnv  5625  f1oresrab  5661  fsn2  5670  xpsng  5671  fnressn  5682  fsnunf  5696  foeqcnvco  5769  isores1  5793  isoini2  5798  riota5f  5833  riotass2  5835  riotass  5836  ovmpodxf  5978  elopabi  6174  cnvf1o  6204  smores3  6272  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  rdgon  6365  frecabcl  6378  frecsuclem  6385  nnsucsssuc  6471  nnsucuniel  6474  erref  6533  iserd  6539  swoer  6541  swoord1  6542  swoord2  6543  erth  6557  erthi  6559  eroveu  6604  pmresg  6654  mapsn  6668  fndmeng  6788  xpen  6823  phplem4  6833  phplem4on  6845  fidifsnen  6848  dif1en  6857  dif1enen  6858  fisbth  6861  diffisn  6871  ac6sfi  6876  fimax2gtri  6879  en2eqpr  6885  unsnfidcex  6897  unsnfidcel  6898  fiintim  6906  fidcenumlemrks  6930  elfi2  6949  elfir  6950  fiuni  6955  fifo  6957  eqsupti  6973  supisoti  6987  ordiso2  7012  casef  7065  difinfsnlem  7076  ctmlemr  7085  ctssdccl  7088  enumct  7092  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  exmidomni  7118  fodjum  7122  fodjuomnilemres  7124  mkvprop  7134  enmkvlem  7137  enwomnilem  7145  nninfdcinf  7147  nninfwlpoimlemdc  7153  acfun  7184  ccfunen  7226  cc2lem  7228  dfplpq2  7316  ltanqi  7364  ltmnqi  7365  ltaddnq  7369  subhalfnqq  7376  ltbtwnnqq  7377  archnqq  7379  prarloclemarch2  7381  enq0sym  7394  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nnnq0lem1  7408  distrnq0  7421  prarloclemlt  7455  prarloclemn  7461  prarloclemcalc  7464  genplt2i  7472  addnqprllem  7489  addnqprulem  7490  addlocprlemgt  7496  appdivnq  7525  prmuloc2  7529  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemru  7574  prplnqu  7582  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemladdfu  7616  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  archrecnq  7625  archrecpr  7626  caucvgprlemk  7627  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprprlemk  7645  caucvgprprlemnkeqj  7652  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemexbt  7668  caucvgprprlemexb  7669  caucvgprprlem1  7671  caucvgprprlem2  7672  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  prsrlem1  7704  addgt0sr  7737  srpospr  7745  prsrriota  7750  caucvgsrlemgt1  7757  caucvgsrlemoffgt1  7761  caucvgsr  7764  mappsrprg  7766  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  recriota  7852  axsuploc  7992  lelttr  8008  ltletr  8009  ltnsymd  8039  lensymd  8041  cnegexlem3  8096  cnegex2  8098  addcanad  8105  addcan2ad  8106  negcon1ad  8225  negne0d  8228  negrebd  8229  subeq0d  8238  subne0ad  8241  neg11d  8242  subcand  8271  subcan2d  8272  ltadd2  8338  ltadd2dd  8341  add20  8393  ltnegcon1d  8444  ltnegcon2d  8445  lenegcon1d  8446  lenegcon2d  8447  subled  8467  lesubd  8468  ltsub23d  8469  ltsub13d  8470  ltadd1dd  8475  ltsub1dd  8476  ltsub2dd  8477  leadd1dd  8478  leadd2dd  8479  lesub1dd  8480  lesub2dd  8481  recexre  8497  apreap  8506  ltmul1a  8510  reapmul1  8514  cru  8521  apreim  8522  mulge0  8538  leltap  8544  negap0d  8550  ltleap  8551  ltapd  8557  ap0gt0  8559  ap0gt0d  8560  mulcanapad  8581  mulcanap2ad  8582  eqnegad  8651  diveqap0d  8714  diveqap1d  8715  divap1d  8718  rec11apd  8728  div11apd  8748  div2subap  8754  recgt0  8766  prodgt0  8768  lemul1a  8774  lemulge12  8783  lt2msq1  8801  lediv12a  8810  recreclt  8816  nn1suc  8897  nnnlt1  8904  nn2ge  8911  nn1gt1  8912  nnrecl  9133  nn0nlt0  9161  elnn0z  9225  nn0negleid  9280  elz2  9283  nn0n0n1ge2b  9291  nnm1ge0  9298  nn0ge0div  9299  zextle  9303  suprzclex  9310  nn0ind-raph  9329  zindd  9330  uzneg  9505  eluzadd  9515  eluzsub  9516  uzm1  9517  uz3m2nn  9532  supminfex  9556  infregelbex  9557  nn01to3  9576  ltrec1d  9674  lerec2d  9675  ledivdivd  9679  divge1  9680  ltmul1dd  9709  ltmul2dd  9710  ltdiv1dd  9711  lediv1dd  9712  ltdiv23d  9714  lediv23d  9715  nn0ledivnn  9724  addlelt  9725  xrlelttr  9763  xrltletr  9764  xaddass2  9827  xltadd1  9833  xlt2add  9837  ixxdisj  9860  icoshftf1o  9948  icodisj  9949  lincmb01cmp  9960  iccf1o  9961  uzsubsubfz  10003  fzdisj  10008  fzopth  10017  fznatpl1  10032  fzsuc2  10035  fzp1disj  10036  fzrev2i  10042  uzdisj  10049  fseq1p1m1  10050  fzm1  10056  fzneuz  10057  fzp1nel  10060  fzrevral  10061  fznn0sub2  10084  fz0fzdiffz0  10086  difelfzle  10090  difelfznle  10091  nn0disj  10094  fzonnsub  10125  fzodisj  10134  fzouzdisj  10136  eluzgtdifelfzo  10153  ubmelfzo  10156  fzonn0p1p1  10169  ubmelm1fzo  10182  fzostep1  10193  exfzdc  10196  subfzo0  10198  qtri3or  10199  exbtwnzlemex  10206  rebtwn2z  10211  qbtwnrelemcalc  10212  qbtwnre  10213  qavgle  10215  apbtwnz  10230  flid  10240  flqwordi  10244  flqmulnn0  10255  flhalf  10258  flltdivnn0lt  10260  fldiv4p1lem1div2  10261  intfracq  10276  flqdiv  10277  flqpmodeq  10283  modqmulnn  10298  mulqaddmodid  10320  modqmuladdim  10323  modqmuladdnn0  10324  m1modge3gt1  10327  q2submod  10341  modaddmodup  10343  modqsubdir  10349  modqeqmodmin  10350  modfzo0difsn  10351  uzennn  10392  uzsinds  10398  monoord2  10433  ser3mono  10434  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemqf1o  10449  iseqf1olemqk  10450  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemp  10458  ser3le  10474  exp3val  10478  expnegap0  10484  expgt1  10514  ltexp2a  10528  le2sq2  10551  nnlesq  10579  qsqeqor  10586  bernneq  10596  expnbnd  10599  expnlbnd  10600  expnlbnd2  10601  expeq0d  10605  sq11d  10642  nn0ltexp2  10644  expcand  10651  nn0opthd  10656  facdiv  10672  faclbnd6  10678  facubnd  10679  facavg  10680  bcval4  10686  bcp1nk  10696  bcval5  10697  bcpasc  10700  hashennnuni  10713  focdmex  10721  isfinite4im  10727  hashnncl  10730  hashunlem  10739  fiprsshashgt1  10752  hashfzp1  10759  zfz1isolemiso  10774  seq3coll  10777  seq3shft  10802  cjth  10810  cjdivap  10873  cjne0d  10911  cjap0d  10912  cvg1nlemcxze  10946  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniq  10959  resqrexlemover  10974  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc2  10979  resqrexlemcalc3  10980  resqrexlemnmsq  10981  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemglsq  10986  resqrexlemga  10987  leabs  11038  absrele  11047  nn0abscl  11049  ltabs  11051  abslt  11052  absle  11053  abstri  11068  amgm2  11082  sqr11d  11137  abs00d  11150  maxabsle  11168  maxabslemlub  11171  maxleastlt  11179  maxltsup  11182  2zsupmax  11189  minmax  11193  2zinfmin  11206  xrmaxleim  11207  xrmaxiflemlub  11211  xrmaxiflemcom  11212  xrmaxiflemval  11213  xrmaxleastlt  11219  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  xrminmax  11228  xrmin1inf  11230  xrmin2inf  11231  xrmineqinf  11232  climi  11250  reccn2ap  11276  climge0  11288  climle  11297  climserle  11308  climrecvg1n  11311  fz1f1o  11338  summodclem3  11343  summodclem2a  11344  summodc  11346  fisumss  11355  fsum0diaglem  11403  mptfzshft  11405  fsumrev  11406  fisum0diag2  11410  fsumlessfi  11423  fsumle  11426  fsumlt  11427  isumsplit  11454  isumrpcl  11457  expcnvap0  11465  geosergap  11469  pwm1geoserap1  11471  absgtap  11473  geolim  11474  geolim2  11475  georeclim  11476  geoisumr  11481  geoisum1c  11483  cvgratnnlembern  11486  cvgratnnlemseq  11489  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  cvgratz  11495  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodmodclem2a  11539  prodmodc  11541  zproddc  11542  fprodntrivap  11547  fprodf1o  11551  fprodssdc  11553  fprodsplitdc  11559  fprodrev  11582  fprodmodd  11604  efcllemp  11621  ege2le3  11634  eftlcvg  11650  eftlub  11653  efltim  11661  eflegeo  11664  tanaddap  11702  sinbnd  11715  cosbnd  11716  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  cos01gt0  11725  cos12dec  11730  eirraplem  11739  zdvdsdc  11774  dvdstr  11790  dvdsadd2b  11802  dvdslelemd  11803  divconjdvds  11809  alzdvds  11814  dvdsext  11815  fzm1ndvds  11816  fzo0dvdseq  11817  zeo3  11827  even2n  11833  mod2eq1n2dvds  11838  nn0ehalf  11862  nnehalf  11863  nno  11865  nn0oddm1d2  11868  divalglemnqt  11879  divalglemex  11881  divalglemeuneg  11882  divalg2  11885  divalgmod  11886  flodddiv4t2lthalf  11896  zsupcllemstep  11900  infssuzex  11904  zsupssdc  11909  dvdsbnd  11911  gcdsupex  11912  gcdsupcl  11913  gcddvds  11918  divgcdz  11926  divgcdnn  11930  gcd0id  11934  gcdneg  11937  gcd1  11942  dvdsgcdidd  11949  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmo  11961  bezoutlemsup  11964  dfgcd3  11965  bezout  11966  dfgcd2  11969  mulgcd  11971  sqgcd  11984  dvdssqlem  11985  bezoutr1  11988  uzwodc  11992  lcmval  12017  lcmcllem  12021  dvdslcm  12023  lcmgcdlem  12031  lcmdvds  12033  lcmgcdeq  12037  ncoprmgcdne1b  12043  mulgcddvds  12048  rpmulgcd2  12049  qredeu  12051  rpdvds  12053  prmind2  12074  nprm  12077  dvdsnprmd  12079  isprm5lem  12095  isprm5  12096  divgcdodd  12097  isprm6  12101  prmexpb  12105  pw2dvds  12120  pw2dvdseulemle  12121  oddpwdclemdc  12127  sqne2sq  12131  znege1  12132  sqrt2irraplemnn  12133  divnumden  12150  divdenle  12151  qden1elz  12159  nn0sqrtelqelz  12160  hashdvds  12175  crth  12178  phimullem  12179  eulerthlemfi  12182  eulerthlemh  12185  eulerthlemth  12186  eulerth  12187  prmdiv  12189  prmdiveq  12190  hashgcdlem  12192  phisum  12194  odzcllem  12196  odzdvds  12199  odzphi  12200  oddprm  12213  pythagtriplem3  12221  pythagtriplem4  12222  pythagtriplem10  12223  pythagtriplem11  12228  pythagtriplem13  12230  pythagtriplem19  12236  pcprendvds  12244  pcprendvds2  12245  pcpre1  12246  pcpremul  12247  pceulem  12248  pceu  12249  pczpre  12251  pcmul  12255  pcdiv  12256  pcqmul  12257  pcqdiv  12261  pcexp  12263  pcidlem  12276  pcneg  12278  pcdvdstr  12280  pcgcd1  12281  pc2dvds  12283  dvdsprmpweq  12288  dvdsprmpweqle  12290  pcaddlem  12292  pcadd  12293  pcmpt  12295  fldivp1  12300  pcfaclem  12301  pcfac  12302  pcbc  12303  qexpz  12304  oddprmdvds  12306  pockthlem  12308  pockthg  12309  infpnlem2  12312  1arith  12319  4sqlem9  12338  4sqlem10  12339  oddennn  12347  ennnfonelemk  12355  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemrnh  12371  ennnfonelemen  12376  ennnfonelemim  12379  ctinfomlemom  12382  ctiunctlemf  12393  ssnnctlemct  12401  nninfdclemcl  12403  nninfdclemp1  12405  nninfdclemlt  12406  unbendc  12409  mgmb1mgm1  12622  mgm1  12624  mgmidsssn0  12638  sgrp1  12651  sgrpidmndm  12656  ismndd  12673  mhmpropd  12689  isgrpd2e  12726  grpidd2  12744  isgrpinv  12756  grpinvinv  12766  ntridm  12920  ntrtop  12922  ntrcls0  12925  ntr0  12928  isopn3i  12929  neiss2  12936  opnneiss  12952  topssnei  12956  cnpf2  13001  icnpimaex  13005  lmcvg  13011  iscnp4  13012  cncnp  13024  cnptopresti  13032  lmfss  13038  lmtopcnp  13044  hmeores  13109  bldisj  13195  xblss2ps  13198  xblss2  13199  blhalf  13202  blssps  13221  blss  13222  ssblex  13225  blpnfctr  13233  xmetresbl  13234  mopni2  13277  bdxmet  13295  bdbl  13297  xmetxpbl  13302  metcnpi  13309  metcnpi2  13310  tgioo  13340  rescncf  13362  mulcncflem  13384  cnopnap  13388  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeu  13395  dedekindicclemuub  13398  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemicc  13404  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthdec  13416  limcimolemlt  13427  cnplimcim  13430  cnplimclemr  13432  limccnpcntop  13438  limccnp2cntop  13440  limccoap  13441  dvfgg  13451  dvidlemap  13454  dvaddxxbr  13459  dvmulxxbr  13460  dvaddxx  13461  dvmulxx  13462  dviaddf  13463  dvimulf  13464  dvcoapbr  13465  dvcjbr  13466  dvcj  13467  dvrecap  13471  dvmptclx  13474  dveflem  13481  reeff1oleme  13487  eflt  13490  sin0pilem1  13496  pilem3  13498  cosq14gt0  13547  coseq0negpitopi  13551  tangtx  13553  coskpi  13563  cosordlem  13564  cosq34lt1  13565  relogef  13579  logrpap0d  13593  rplogcl  13594  logge0  13595  logdivlti  13596  cxplt3  13634  rpabscxpbnd  13653  lgslem1  13695  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsvalmod  13714  lgsfcl3  13716  lgsmod  13721  lgsdirprm  13729  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  2sqlem3  13747  2sqlem4  13748  2sqlem8  13753  bj-charfunr  13845  pwf1oexmid  14032  subctctexmid  14034  pw1nct  14036  nnsf  14038  peano4nninf  14039  nninfsellemeq  14047  cvgcmp2nlemabs  14064  iooref1o  14066  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  apdifflemf  14078  apdifflemr  14079  apdiff  14080  iswomninnlem  14081  redcwlpo  14087  redc0  14089  reap0  14090  nconstwlpolemgt0  14095  neapmkvlem  14098  supfz  14100  inffz  14101