Theorem mpbid 147

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 144	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbii  148  annimdc  943  mpbi2and  949  bilukdc  1438  equs5or  1876  eqtrd  2262  eleqtrd  2308  neeqtrd  2428  3netr3d  2432  rexlimd2  2646  raleqtrdv  2736  rexeqtrdv  2737  ceqsalt  2826  vtoclgft  2851  vtoclegft  2875  elrab3t  2958  eueq2dc  2976  sbceq1dd  3034  csbiedf  3165  sseqtrd  3262  3sstr3d  3268  ifbothdadc  3636  snssd  3813  dfnfc2  3906  breqdi  4098  breqtrd  4109  3brtr3d  4114  csbexga  4212  reuhypd  4562  reg2exmidlema  4626  elirr  4633  en2lp  4646  onsucuni2  4656  finds  4692  iota4  5298  iota4an  5299  funimaexglem  5404  fneu  5427  fco2  5490  fssres2  5503  fresin  5504  feu  5508  f1orescnv  5588  resdif  5594  funcocnv2  5597  f1oprg  5617  fvelrnb  5681  fimacnv  5764  f1oresrab  5800  fsn2  5809  xpsng  5810  funopsn  5817  fnressn  5825  fsnunf  5839  foeqcnvco  5914  isores1  5938  isoini2  5943  riota5f  5981  riotass2  5983  riotass  5984  ovmpodxf  6130  uchoice  6283  elopabi  6341  cnvf1o  6371  smores3  6439  tfrlemisucaccv  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  rdgon  6532  frecabcl  6545  frecsuclem  6552  nnsucsssuc  6638  nnsucuniel  6641  erref  6700  iserd  6706  swoer  6708  swoord1  6709  swoord2  6710  erth  6726  erthi  6728  eroveu  6773  pmresg  6823  mapsn  6837  fndmeng  6963  xpen  7006  phplem4  7016  phplem4on  7029  fidifsnen  7032  dif1en  7041  dif1enen  7042  fisbth  7045  diffisn  7055  ac6sfi  7060  fimax2gtri  7063  en2eqpr  7069  unsnfidcex  7082  unsnfidcel  7083  prfidceq  7090  fiintim  7093  fidcenumlemrks  7120  elfi2  7139  elfir  7140  fiuni  7145  fifo  7147  eqsupti  7163  supisoti  7177  ordiso2  7202  casef  7255  difinfsnlem  7266  ctmlemr  7275  ctssdccl  7278  enumct  7282  nninfninc  7290  nnnninfeq  7295  nnnninfeq2  7296  enomnilem  7305  exmidomni  7309  fodjum  7313  fodjuomnilemres  7315  mkvprop  7325  enmkvlem  7328  enwomnilem  7336  nninfdcinf  7338  nninfwlpoimlemdc  7344  nninfinfwlpolem  7345  pr1or2  7367  acfun  7389  2omotaplemap  7443  exmidmotap  7447  ccfunen  7450  cc2lem  7452  dfplpq2  7541  ltanqi  7589  ltmnqi  7590  ltaddnq  7594  subhalfnqq  7601  ltbtwnnqq  7602  archnqq  7604  prarloclemarch2  7606  enq0sym  7619  enq0ref  7620  enq0tr  7621  nqnq0pi  7625  nnnq0lem1  7633  distrnq0  7646  prarloclemlt  7680  prarloclemn  7686  prarloclemcalc  7689  genplt2i  7697  addnqprllem  7714  addnqprulem  7715  addlocprlemgt  7721  appdivnq  7750  prmuloc2  7754  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemru  7799  prplnqu  7807  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemladdfu  7841  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  archrecnq  7850  archrecpr  7851  caucvgprlemk  7852  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprprlemk  7870  caucvgprprlemnkeqj  7877  caucvgprprlemnbj  7880  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemopu  7886  caucvgprprlemexbt  7893  caucvgprprlemexb  7894  caucvgprprlem1  7896  caucvgprprlem2  7897  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  suplocexprlemlub  7911  prsrlem1  7929  addgt0sr  7962  srpospr  7970  prsrriota  7975  caucvgsrlemgt1  7982  caucvgsrlemoffgt1  7986  caucvgsr  7989  mappsrprg  7991  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  recriota  8077  axsuploc  8219  lelttr  8235  ltletr  8236  ltnsymd  8266  lensymd  8268  cnegexlem3  8323  cnegex2  8325  addcanad  8332  addcan2ad  8333  negcon1ad  8452  negne0d  8455  negrebd  8456  subeq0d  8465  subne0ad  8468  neg11d  8469  subcand  8498  subcan2d  8499  ltadd2  8566  ltadd2dd  8569  add20  8621  ltnegcon1d  8672  ltnegcon2d  8673  lenegcon1d  8674  lenegcon2d  8675  subled  8695  lesubd  8696  ltsub23d  8697  ltsub13d  8698  ltadd1dd  8703  ltsub1dd  8704  ltsub2dd  8705  leadd1dd  8706  leadd2dd  8707  lesub1dd  8708  lesub2dd  8709  recexre  8725  apreap  8734  ltmul1a  8738  reapmul1  8742  cru  8749  apreim  8750  mulge0  8766  leltap  8772  negap0d  8778  ltleap  8779  ltapd  8785  ap0gt0  8787  ap0gt0d  8788  mulcanapad  8810  mulcanap2ad  8811  eqnegad  8881  diveqap0d  8944  diveqap1d  8945  divap1d  8948  rec11apd  8958  div11apd  8978  div2subap  8984  recgt0  8997  prodgt0  8999  lemul1a  9005  lemulge12  9014  lt2msq1  9032  lediv12a  9041  recreclt  9047  nn1suc  9129  nnnlt1  9136  nn2ge  9143  nn1gt1  9144  nnrecl  9367  nn0nlt0  9395  elnn0z  9459  nnnle0  9495  nn0negleid  9515  elz2  9518  nn0n0n1ge2b  9526  nnm1ge0  9533  nn0ge0div  9534  zextle  9538  suprzclex  9545  nn0ind-raph  9564  zindd  9565  uzneg  9741  eluzadd  9751  eluzsub  9752  uzm1  9753  uz3m2nn  9768  supminfex  9792  infregelbex  9793  nn01to3  9812  irrmulap  9843  ltrec1d  9913  lerec2d  9914  ledivdivd  9918  divge1  9919  ltmul1dd  9948  ltmul2dd  9949  ltdiv1dd  9950  lediv1dd  9951  ltdiv23d  9953  lediv23d  9954  nn0ledivnn  9963  addlelt  9964  xrlelttr  10002  xrltletr  10003  xaddass2  10066  xltadd1  10072  xlt2add  10076  ixxdisj  10099  icoshftf1o  10187  icodisj  10188  lincmb01cmp  10199  iccf1o  10200  uzsubsubfz  10243  fzdisj  10248  fzopth  10257  fznatpl1  10272  fzsuc2  10275  fzp1disj  10276  fzrev2i  10282  uzdisj  10289  fseq1p1m1  10290  fzm1  10296  fzneuz  10297  fzp1nel  10300  fzrevral  10301  fznn0sub2  10324  fz0fzdiffz0  10326  difelfzle  10330  difelfznle  10331  nn0disj  10334  fzonnsub  10367  fzodisj  10376  fzouzdisj  10378  fzoun  10379  eluzgtdifelfzo  10403  ubmelfzo  10406  fzonn0p1p1  10419  ubmelm1fzo  10432  fzostep1  10443  exfzdc  10446  subfzo0  10448  zsupcllemstep  10449  infssuzex  10453  zsupssdc  10458  qtri3or  10460  exbtwnzlemex  10469  rebtwn2z  10474  qbtwnrelemcalc  10475  qbtwnre  10476  qavgle  10478  apbtwnz  10494  flid  10504  flqwordi  10508  flqmulnn0  10519  flhalf  10522  flltdivnn0lt  10524  fldiv4p1lem1div2  10525  intfracq  10542  flqdiv  10543  flqpmodeq  10549  modqmulnn  10564  mulqaddmodid  10586  modqmuladdim  10589  modqmuladdnn0  10590  m1modge3gt1  10593  q2submod  10607  modaddmodup  10609  modqsubdir  10615  modqeqmodmin  10616  modfzo0difsn  10617  uzennn  10658  uzsinds  10666  monoord2  10708  ser3mono  10709  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  iseqf1olemqf1o  10728  iseqf1olemqk  10729  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1olemp  10737  seqf1oglem1  10741  seqf1oglem2  10742  ser3le  10759  exp3val  10763  expnegap0  10769  expgt1  10799  ltexp2a  10813  le2sq2  10837  nnlesq  10865  qsqeqor  10872  bernneq  10882  expnbnd  10885  expnlbnd  10886  expnlbnd2  10887  expeq0d  10891  sq11d  10928  nn0ltexp2  10931  expcand  10939  nn0opthd  10944  facdiv  10960  faclbnd6  10966  facubnd  10967  facavg  10968  bcval4  10974  bcp1nk  10984  bcval5  10985  bcpasc  10988  hashennnuni  11001  isfinite4im  11014  hashnncl  11017  hashunlem  11026  fiprsshashgt1  11039  hashfzp1  11046  zfz1isolemiso  11061  seq3coll  11064  hash2en  11065  iswrdiz  11078  wrdffz  11092  ffz0iswrdnn0  11098  ccatval21sw  11140  ccatass  11143  swrdf  11187  swrdlend  11190  ccatswrd  11202  swrdccat2  11203  pfxsuffeqwrdeq  11230  ccatpfx  11233  ccats1pfxeq  11246  cats1un  11253  wrdind  11254  wrd2ind  11255  pfxccatin12  11265  swrdccat  11267  s2dmg  11322  seq3shft  11349  cjth  11357  cjdivap  11420  cjne0d  11458  cjap0d  11459  cvg1nlemcxze  11493  cvg1nlemcau  11495  cvg1nlemres  11496  recvguniq  11506  resqrexlemover  11521  resqrexlemdecn  11523  resqrexlemlo  11524  resqrexlemcalc2  11526  resqrexlemcalc3  11527  resqrexlemnmsq  11528  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemglsq  11533  resqrexlemga  11534  leabs  11585  absrele  11594  nn0abscl  11596  ltabs  11598  abslt  11599  absle  11600  abstri  11615  amgm2  11629  sqr11d  11684  abs00d  11697  maxabsle  11715  maxabslemlub  11718  maxleastlt  11726  maxltsup  11729  2zsupmax  11737  minmax  11741  2zinfmin  11754  xrmaxleim  11755  xrmaxiflemlub  11759  xrmaxiflemcom  11760  xrmaxiflemval  11761  xrmaxleastlt  11767  xrmaxltsup  11769  xrmaxaddlem  11771  xrmaxadd  11772  xrminmax  11776  xrmin1inf  11778  xrmin2inf  11779  xrmineqinf  11780  climi  11798  reccn2ap  11824  climge0  11836  climle  11845  climserle  11856  climrecvg1n  11859  fz1f1o  11886  summodclem3  11891  summodclem2a  11892  summodc  11894  fisumss  11903  fsum0diaglem  11951  mptfzshft  11953  fsumrev  11954  fisum0diag2  11958  fsumlessfi  11971  fsumle  11974  fsumlt  11975  isumsplit  12002  isumrpcl  12005  expcnvap0  12013  geosergap  12017  pwm1geoserap1  12019  absgtap  12021  geolim  12022  geolim2  12023  georeclim  12024  geoisumr  12029  geoisum1c  12031  cvgratnnlembern  12034  cvgratnnlemseq  12037  cvgratnnlemsumlt  12039  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratnn  12042  cvgratz  12043  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodmodclem2a  12087  prodmodc  12089  zproddc  12090  fprodntrivap  12095  fprodf1o  12099  fprodssdc  12101  fprodsplitdc  12107  fprodrev  12130  fprodmodd  12152  efcllemp  12169  ege2le3  12182  eftlcvg  12198  eftlub  12201  efltim  12209  eflegeo  12212  tanaddap  12250  sinbnd  12263  cosbnd  12264  sin01bnd  12268  cos01bnd  12269  sinltxirr  12272  sin01gt0  12273  cos01gt0  12274  cos12dec  12279  eirraplem  12288  zdvdsdc  12323  dvdstr  12339  dvdsadd2b  12351  fsumdvds  12353  dvdslelemd  12354  divconjdvds  12360  alzdvds  12365  dvdsext  12366  fzm1ndvds  12367  fzo0dvdseq  12368  3dvds  12375  zeo3  12379  even2n  12385  mod2eq1n2dvds  12390  nn0ehalf  12414  nnehalf  12415  nno  12417  nn0oddm1d2  12420  divalglemnqt  12431  divalglemex  12433  divalglemeuneg  12434  divalg2  12437  divalgmod  12438  flodddiv4t2lthalf  12450  bitsfzolem  12465  bitsfzo  12466  bitsmod  12467  bitsfi  12468  bitscmp  12469  bitsinv1lem  12472  bitsinv1  12473  dvdsbnd  12477  gcdsupex  12478  gcdsupcl  12479  gcddvds  12484  divgcdz  12492  divgcdnn  12496  gcd0id  12500  gcdneg  12503  gcd1  12508  dvdsgcdidd  12515  bezoutlemnewy  12517  bezoutlemstep  12518  bezoutlemmo  12527  bezoutlemsup  12530  dfgcd3  12531  bezout  12532  dfgcd2  12535  mulgcd  12537  sqgcd  12550  dvdssqlem  12551  bezoutr1  12554  uzwodc  12558  nninfctlemfo  12561  lcmval  12585  lcmcllem  12589  dvdslcm  12591  lcmgcdlem  12599  lcmdvds  12601  lcmgcdeq  12605  ncoprmgcdne1b  12611  mulgcddvds  12616  rpmulgcd2  12617  qredeu  12619  rpdvds  12621  prmind2  12642  nprm  12645  dvdsnprmd  12647  isprm5lem  12663  isprm5  12664  divgcdodd  12665  isprm6  12669  prmexpb  12673  pw2dvds  12688  pw2dvdseulemle  12689  oddpwdclemdc  12695  sqne2sq  12699  znege1  12700  sqrt2irraplemnn  12701  divnumden  12718  divdenle  12719  qden1elz  12727  nn0sqrtelqelz  12728  hashdvds  12743  crth  12746  phimullem  12747  eulerthlemfi  12750  eulerthlemh  12753  eulerthlemth  12754  eulerth  12755  prmdiv  12757  prmdiveq  12758  hashgcdlem  12760  dvdsfi  12761  phisum  12763  odzcllem  12765  odzdvds  12768  odzphi  12769  oddprm  12782  pythagtriplem3  12790  pythagtriplem4  12791  pythagtriplem10  12792  pythagtriplem11  12797  pythagtriplem13  12799  pythagtriplem19  12805  pcprendvds  12813  pcprendvds2  12814  pcpre1  12815  pcpremul  12816  pceulem  12817  pceu  12818  pczpre  12820  pcmul  12824  pcdiv  12825  pcqmul  12826  pcqdiv  12830  pcexp  12832  pcidlem  12846  pcneg  12848  pcdvdstr  12850  pcgcd1  12851  pc2dvds  12853  dvdsprmpweq  12858  dvdsprmpweqle  12860  pcaddlem  12862  pcadd  12863  pcadd2  12864  pcmpt  12866  fldivp1  12871  pcfaclem  12872  pcfac  12873  pcbc  12874  qexpz  12875  oddprmdvds  12877  pockthlem  12879  pockthg  12880  infpnlem2  12883  1arith  12890  4sqlem9  12909  4sqlem10  12910  4sqlem11  12924  4sqlem12  12925  4sqlem13m  12926  4sqlem14  12927  4sqlem16  12929  oddennn  12963  ennnfonelemk  12971  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemrnh  12987  ennnfonelemen  12992  ennnfonelemim  12995  ctinfomlemom  12998  ctiunctlemf  13009  ssnnctlemct  13017  nninfdclemcl  13019  nninfdclemp1  13021  nninfdclemlt  13022  unbendc  13025  prdsbascl  13322  pwselbas  13327  mgmb1mgm1  13401  mgm1  13403  mgmidsssn0  13417  gsumfzval  13424  gsumress  13428  gsum0g  13429  gsumval2  13430  sgrp1  13444  sgrpidmndm  13453  ismndd  13470  prds0g  13482  mhmpropd  13499  resmhm  13520  resmhm2b  13522  gsumwsubmcl  13529  gsumwmhm  13531  isgrpd2e  13553  grpidd2  13574  isgrpinv  13587  grpinvinv  13600  grpidssd  13609  grpinvssd  13610  mulgval  13659  mulgfng  13661  mulgnegnn  13669  subg0  13717  issubg4m  13730  nsgconj  13743  1nsgtrivd  13756  eqgen  13764  eqgcpbl  13765  qus0  13772  ghmid  13786  resghm  13797  ghmnsgpreima  13806  kerf1ghm  13811  conjsubgen  13815  conjnmz  13816  imasabl  13873  rnglz  13908  rngrz  13909  qusrng  13921  issrgid  13944  srg1zr  13950  ringcl  13976  isringid  13988  ringcom  13994  ringpropd  14001  ringlz  14006  ringrz  14007  ring1  14022  opprrng  14040  opprring  14042  dvdsrcld  14061  unitcld  14072  unitmulcl  14077  unitgrp  14080  unitnegcl  14094  rhmmul  14128  isrhm2d  14129  rhmdvdsr  14139  rhmopp  14140  elrhmunit  14141  rhmunitinv  14142  subrgugrp  14204  aprsym  14248  islmodd  14257  lmod0vs  14285  lmodfopne  14290  lmodcom  14297  lssclg  14328  lspsnel5a  14374  lspsneq0b  14391  lsslsp  14393  sraring  14413  sralmod  14414  rspssp  14458  rnglidlmsgrp  14461  2idlcpblrng  14487  gsumfzfsumlem0  14550  zncrng  14609  znzrh2  14610  znzrhfo  14612  znf1o  14615  znfi  14619  znhash  14620  znidom  14621  znidomb  14622  znunit  14623  znrrg  14624  psrbaglesuppg  14636  psrelbas  14639  psrelbasfi  14640  psrgrp  14649  psr0  14650  psr1clfi  14652  mplsubgfilemcl  14663  mplsubgfileminv  14664  ntridm  14800  ntrtop  14802  ntrcls0  14805  ntr0  14808  isopn3i  14809  neiss2  14816  opnneiss  14832  topssnei  14836  cnpf2  14881  icnpimaex  14885  lmcvg  14891  iscnp4  14892  cncnp  14904  cnptopresti  14912  lmfss  14918  lmtopcnp  14924  hmeores  14989  bldisj  15075  xblss2ps  15078  xblss2  15079  blhalf  15082  blssps  15101  blss  15102  ssblex  15105  blpnfctr  15113  xmetresbl  15114  mopni2  15157  bdxmet  15175  bdbl  15177  xmetxpbl  15182  metcnpi  15189  metcnpi2  15190  tgioo  15228  rescncf  15255  mulcncflem  15281  cnopnap  15285  dedekindeulemuub  15291  dedekindeulemloc  15293  dedekindeulemlu  15295  dedekindeu  15297  dedekindicclemuub  15300  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicclemicc  15306  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthdec  15318  ivthreinc  15319  hovergt0  15324  dich0  15326  limcimolemlt  15338  cnplimcim  15341  cnplimclemr  15343  limccnpcntop  15349  limccnp2cntop  15351  limccoap  15352  dvfgg  15362  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvaddxxbr  15375  dvmulxxbr  15376  dvaddxx  15377  dvmulxx  15378  dviaddf  15379  dvimulf  15380  dvcoapbr  15381  dvcjbr  15382  dvcj  15383  dvrecap  15387  dvmptclx  15392  dveflem  15400  elply2  15409  plyf  15411  plyaddlem  15423  plymullem  15424  plycoeid3  15431  plyco  15433  plycj  15435  dvply1  15439  dvply2g  15440  reeff1oleme  15446  eflt  15449  sin0pilem1  15455  pilem3  15457  cosq14gt0  15506  coseq0negpitopi  15510  tangtx  15512  coskpi  15522  cosordlem  15523  cosq34lt1  15524  relogef  15538  logrpap0d  15552  rplogcl  15553  logge0  15554  logdivlti  15555  cxplt3  15594  rpabscxpbnd  15614  dvdsppwf1o  15663  fsumdvdsmul  15665  mersenne  15671  perfect1  15672  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgslem1  15679  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  lgsvalmod  15698  lgsfcl3  15700  lgsmod  15705  lgsdirprm  15713  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem3  15742  gausslemma2dlem4  15743  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem1  15760  lgsquad2lem2  15761  lgsquad3  15763  2lgslem1c  15769  2lgsoddprm  15792  2sqlem3  15796  2sqlem4  15797  2sqlem8  15802  lpvtx  15879  umgrnloopv  15914  umgredgne  15948  ausgrusgrien  15969  wlkcompim  16063  wlkvtxedg  16074  bj-charfunr  16173  2omap  16359  pw1map  16361  pwf1oexmid  16365  subctctexmid  16366  domomsubct  16367  pw1nct  16369  nnsf  16371  peano4nninf  16372  nninfsellemeq  16380  nnnninfex  16388  cvgcmp2nlemabs  16400  iooref1o  16402  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  trirec0  16412  apdifflemf  16414  apdifflemr  16415  apdiff  16416  iswomninnlem  16417  redcwlpo  16423  redc0  16425  reap0  16426  nconstwlpolemgt0  16432  neapmkvlem  16435  ltlenmkv  16438  supfz  16439  inffz  16440