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  940  mpbi2and  946  bilukdc  1416  equs5or  1853  eqtrd  2238  eleqtrd  2284  neeqtrd  2404  3netr3d  2408  rexlimd2  2621  raleqtrdv  2710  rexeqtrdv  2711  ceqsalt  2798  vtoclgft  2823  vtoclegft  2845  elrab3t  2928  eueq2dc  2946  sbceq1dd  3004  csbiedf  3134  sseqtrd  3231  3sstr3d  3237  ifbothdadc  3604  snssd  3778  dfnfc2  3868  breqdi  4060  breqtrd  4071  3brtr3d  4076  csbexga  4173  reuhypd  4519  reg2exmidlema  4583  elirr  4590  en2lp  4603  onsucuni2  4613  finds  4649  iota4  5252  iota4an  5253  funimaexglem  5358  fneu  5381  fco2  5444  fssres2  5455  fresin  5456  feu  5460  f1orescnv  5540  resdif  5546  funcocnv2  5549  f1oprg  5568  fvelrnb  5628  fimacnv  5711  f1oresrab  5747  fsn2  5756  xpsng  5757  funopsn  5764  fnressn  5772  fsnunf  5786  foeqcnvco  5861  isores1  5885  isoini2  5890  riota5f  5926  riotass2  5928  riotass  5929  ovmpodxf  6073  uchoice  6225  elopabi  6283  cnvf1o  6313  smores3  6381  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  rdgon  6474  frecabcl  6487  frecsuclem  6494  nnsucsssuc  6580  nnsucuniel  6583  erref  6642  iserd  6648  swoer  6650  swoord1  6651  swoord2  6652  erth  6668  erthi  6670  eroveu  6715  pmresg  6765  mapsn  6779  fndmeng  6904  xpen  6944  phplem4  6954  phplem4on  6966  fidifsnen  6969  dif1en  6978  dif1enen  6979  fisbth  6982  diffisn  6992  ac6sfi  6997  fimax2gtri  7000  en2eqpr  7006  unsnfidcex  7019  unsnfidcel  7020  prfidceq  7027  fiintim  7030  fidcenumlemrks  7057  elfi2  7076  elfir  7077  fiuni  7082  fifo  7084  eqsupti  7100  supisoti  7114  ordiso2  7139  casef  7192  difinfsnlem  7203  ctmlemr  7212  ctssdccl  7215  enumct  7219  nninfninc  7227  nnnninfeq  7232  nnnninfeq2  7233  enomnilem  7242  exmidomni  7246  fodjum  7250  fodjuomnilemres  7252  mkvprop  7262  enmkvlem  7265  enwomnilem  7273  nninfdcinf  7275  nninfwlpoimlemdc  7281  nninfinfwlpolem  7282  acfun  7321  2omotaplemap  7371  exmidmotap  7375  ccfunen  7378  cc2lem  7380  dfplpq2  7469  ltanqi  7517  ltmnqi  7518  ltaddnq  7522  subhalfnqq  7529  ltbtwnnqq  7530  archnqq  7532  prarloclemarch2  7534  enq0sym  7547  enq0ref  7548  enq0tr  7549  nqnq0pi  7553  nnnq0lem1  7561  distrnq0  7574  prarloclemlt  7608  prarloclemn  7614  prarloclemcalc  7617  genplt2i  7625  addnqprllem  7642  addnqprulem  7643  addlocprlemgt  7649  appdivnq  7678  prmuloc2  7682  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemru  7727  prplnqu  7735  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemladdfu  7769  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  archrecnq  7778  archrecpr  7779  caucvgprlemk  7780  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprprlemk  7798  caucvgprprlemnkeqj  7805  caucvgprprlemnbj  7808  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemexbt  7821  caucvgprprlemexb  7822  caucvgprprlem1  7824  caucvgprprlem2  7825  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemub  7838  suplocexprlemlub  7839  prsrlem1  7857  addgt0sr  7890  srpospr  7898  prsrriota  7903  caucvgsrlemgt1  7910  caucvgsrlemoffgt1  7914  caucvgsr  7917  mappsrprg  7919  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  recriota  8005  axsuploc  8147  lelttr  8163  ltletr  8164  ltnsymd  8194  lensymd  8196  cnegexlem3  8251  cnegex2  8253  addcanad  8260  addcan2ad  8261  negcon1ad  8380  negne0d  8383  negrebd  8384  subeq0d  8393  subne0ad  8396  neg11d  8397  subcand  8426  subcan2d  8427  ltadd2  8494  ltadd2dd  8497  add20  8549  ltnegcon1d  8600  ltnegcon2d  8601  lenegcon1d  8602  lenegcon2d  8603  subled  8623  lesubd  8624  ltsub23d  8625  ltsub13d  8626  ltadd1dd  8631  ltsub1dd  8632  ltsub2dd  8633  leadd1dd  8634  leadd2dd  8635  lesub1dd  8636  lesub2dd  8637  recexre  8653  apreap  8662  ltmul1a  8666  reapmul1  8670  cru  8677  apreim  8678  mulge0  8694  leltap  8700  negap0d  8706  ltleap  8707  ltapd  8713  ap0gt0  8715  ap0gt0d  8716  mulcanapad  8738  mulcanap2ad  8739  eqnegad  8809  diveqap0d  8872  diveqap1d  8873  divap1d  8876  rec11apd  8886  div11apd  8906  div2subap  8912  recgt0  8925  prodgt0  8927  lemul1a  8933  lemulge12  8942  lt2msq1  8960  lediv12a  8969  recreclt  8975  nn1suc  9057  nnnlt1  9064  nn2ge  9071  nn1gt1  9072  nnrecl  9295  nn0nlt0  9323  elnn0z  9387  nnnle0  9423  nn0negleid  9443  elz2  9446  nn0n0n1ge2b  9454  nnm1ge0  9461  nn0ge0div  9462  zextle  9466  suprzclex  9473  nn0ind-raph  9492  zindd  9493  uzneg  9669  eluzadd  9679  eluzsub  9680  uzm1  9681  uz3m2nn  9696  supminfex  9720  infregelbex  9721  nn01to3  9740  irrmulap  9771  ltrec1d  9841  lerec2d  9842  ledivdivd  9846  divge1  9847  ltmul1dd  9876  ltmul2dd  9877  ltdiv1dd  9878  lediv1dd  9879  ltdiv23d  9881  lediv23d  9882  nn0ledivnn  9891  addlelt  9892  xrlelttr  9930  xrltletr  9931  xaddass2  9994  xltadd1  10000  xlt2add  10004  ixxdisj  10027  icoshftf1o  10115  icodisj  10116  lincmb01cmp  10127  iccf1o  10128  uzsubsubfz  10171  fzdisj  10176  fzopth  10185  fznatpl1  10200  fzsuc2  10203  fzp1disj  10204  fzrev2i  10210  uzdisj  10217  fseq1p1m1  10218  fzm1  10224  fzneuz  10225  fzp1nel  10228  fzrevral  10229  fznn0sub2  10252  fz0fzdiffz0  10254  difelfzle  10258  difelfznle  10259  nn0disj  10262  fzonnsub  10295  fzodisj  10304  fzouzdisj  10306  eluzgtdifelfzo  10328  ubmelfzo  10331  fzonn0p1p1  10344  ubmelm1fzo  10357  fzostep1  10368  exfzdc  10371  subfzo0  10373  zsupcllemstep  10374  infssuzex  10378  zsupssdc  10383  qtri3or  10385  exbtwnzlemex  10394  rebtwn2z  10399  qbtwnrelemcalc  10400  qbtwnre  10401  qavgle  10403  apbtwnz  10419  flid  10429  flqwordi  10433  flqmulnn0  10444  flhalf  10447  flltdivnn0lt  10449  fldiv4p1lem1div2  10450  intfracq  10467  flqdiv  10468  flqpmodeq  10474  modqmulnn  10489  mulqaddmodid  10511  modqmuladdim  10514  modqmuladdnn0  10515  m1modge3gt1  10518  q2submod  10532  modaddmodup  10534  modqsubdir  10540  modqeqmodmin  10541  modfzo0difsn  10542  uzennn  10583  uzsinds  10591  monoord2  10633  ser3mono  10634  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemab  10649  iseqf1olemqf1o  10653  iseqf1olemqk  10654  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seq3f1olemp  10662  seqf1oglem1  10666  seqf1oglem2  10667  ser3le  10684  exp3val  10688  expnegap0  10694  expgt1  10724  ltexp2a  10738  le2sq2  10762  nnlesq  10790  qsqeqor  10797  bernneq  10807  expnbnd  10810  expnlbnd  10811  expnlbnd2  10812  expeq0d  10816  sq11d  10853  nn0ltexp2  10856  expcand  10864  nn0opthd  10869  facdiv  10885  faclbnd6  10891  facubnd  10892  facavg  10893  bcval4  10899  bcp1nk  10909  bcval5  10910  bcpasc  10913  hashennnuni  10926  isfinite4im  10939  hashnncl  10942  hashunlem  10951  fiprsshashgt1  10964  hashfzp1  10971  zfz1isolemiso  10986  seq3coll  10989  hash2en  10990  iswrdiz  11003  wrdffz  11017  ccatval21sw  11064  ccatass  11067  swrdf  11111  swrdlend  11114  ccatswrd  11126  swrdccat2  11127  pfxsuffeqwrdeq  11152  ccatpfx  11155  seq3shft  11182  cjth  11190  cjdivap  11253  cjne0d  11291  cjap0d  11292  cvg1nlemcxze  11326  cvg1nlemcau  11328  cvg1nlemres  11329  recvguniq  11339  resqrexlemover  11354  resqrexlemdecn  11356  resqrexlemlo  11357  resqrexlemcalc2  11359  resqrexlemcalc3  11360  resqrexlemnmsq  11361  resqrexlemnm  11362  resqrexlemcvg  11363  resqrexlemglsq  11366  resqrexlemga  11367  leabs  11418  absrele  11427  nn0abscl  11429  ltabs  11431  abslt  11432  absle  11433  abstri  11448  amgm2  11462  sqr11d  11517  abs00d  11530  maxabsle  11548  maxabslemlub  11551  maxleastlt  11559  maxltsup  11562  2zsupmax  11570  minmax  11574  2zinfmin  11587  xrmaxleim  11588  xrmaxiflemlub  11592  xrmaxiflemcom  11593  xrmaxiflemval  11594  xrmaxleastlt  11600  xrmaxltsup  11602  xrmaxaddlem  11604  xrmaxadd  11605  xrminmax  11609  xrmin1inf  11611  xrmin2inf  11612  xrmineqinf  11613  climi  11631  reccn2ap  11657  climge0  11669  climle  11678  climserle  11689  climrecvg1n  11692  fz1f1o  11719  summodclem3  11724  summodclem2a  11725  summodc  11727  fisumss  11736  fsum0diaglem  11784  mptfzshft  11786  fsumrev  11787  fisum0diag2  11791  fsumlessfi  11804  fsumle  11807  fsumlt  11808  isumsplit  11835  isumrpcl  11838  expcnvap0  11846  geosergap  11850  pwm1geoserap1  11852  absgtap  11854  geolim  11855  geolim2  11856  georeclim  11857  geoisumr  11862  geoisum1c  11864  cvgratnnlembern  11867  cvgratnnlemseq  11870  cvgratnnlemsumlt  11872  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratnn  11875  cvgratz  11876  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodmodclem2a  11920  prodmodc  11922  zproddc  11923  fprodntrivap  11928  fprodf1o  11932  fprodssdc  11934  fprodsplitdc  11940  fprodrev  11963  fprodmodd  11985  efcllemp  12002  ege2le3  12015  eftlcvg  12031  eftlub  12034  efltim  12042  eflegeo  12045  tanaddap  12083  sinbnd  12096  cosbnd  12097  sin01bnd  12101  cos01bnd  12102  sinltxirr  12105  sin01gt0  12106  cos01gt0  12107  cos12dec  12112  eirraplem  12121  zdvdsdc  12156  dvdstr  12172  dvdsadd2b  12184  fsumdvds  12186  dvdslelemd  12187  divconjdvds  12193  alzdvds  12198  dvdsext  12199  fzm1ndvds  12200  fzo0dvdseq  12201  3dvds  12208  zeo3  12212  even2n  12218  mod2eq1n2dvds  12223  nn0ehalf  12247  nnehalf  12248  nno  12250  nn0oddm1d2  12253  divalglemnqt  12264  divalglemex  12266  divalglemeuneg  12267  divalg2  12270  divalgmod  12271  flodddiv4t2lthalf  12283  bitsfzolem  12298  bitsfzo  12299  bitsmod  12300  bitsfi  12301  bitscmp  12302  bitsinv1lem  12305  bitsinv1  12306  dvdsbnd  12310  gcdsupex  12311  gcdsupcl  12312  gcddvds  12317  divgcdz  12325  divgcdnn  12329  gcd0id  12333  gcdneg  12336  gcd1  12341  dvdsgcdidd  12348  bezoutlemnewy  12350  bezoutlemstep  12351  bezoutlemmo  12360  bezoutlemsup  12363  dfgcd3  12364  bezout  12365  dfgcd2  12368  mulgcd  12370  sqgcd  12383  dvdssqlem  12384  bezoutr1  12387  uzwodc  12391  nninfctlemfo  12394  lcmval  12418  lcmcllem  12422  dvdslcm  12424  lcmgcdlem  12432  lcmdvds  12434  lcmgcdeq  12438  ncoprmgcdne1b  12444  mulgcddvds  12449  rpmulgcd2  12450  qredeu  12452  rpdvds  12454  prmind2  12475  nprm  12478  dvdsnprmd  12480  isprm5lem  12496  isprm5  12497  divgcdodd  12498  isprm6  12502  prmexpb  12506  pw2dvds  12521  pw2dvdseulemle  12522  oddpwdclemdc  12528  sqne2sq  12532  znege1  12533  sqrt2irraplemnn  12534  divnumden  12551  divdenle  12552  qden1elz  12560  nn0sqrtelqelz  12561  hashdvds  12576  crth  12579  phimullem  12580  eulerthlemfi  12583  eulerthlemh  12586  eulerthlemth  12587  eulerth  12588  prmdiv  12590  prmdiveq  12591  hashgcdlem  12593  dvdsfi  12594  phisum  12596  odzcllem  12598  odzdvds  12601  odzphi  12602  oddprm  12615  pythagtriplem3  12623  pythagtriplem4  12624  pythagtriplem10  12625  pythagtriplem11  12630  pythagtriplem13  12632  pythagtriplem19  12638  pcprendvds  12646  pcprendvds2  12647  pcpre1  12648  pcpremul  12649  pceulem  12650  pceu  12651  pczpre  12653  pcmul  12657  pcdiv  12658  pcqmul  12659  pcqdiv  12663  pcexp  12665  pcidlem  12679  pcneg  12681  pcdvdstr  12683  pcgcd1  12684  pc2dvds  12686  dvdsprmpweq  12691  dvdsprmpweqle  12693  pcaddlem  12695  pcadd  12696  pcadd2  12697  pcmpt  12699  fldivp1  12704  pcfaclem  12705  pcfac  12706  pcbc  12707  qexpz  12708  oddprmdvds  12710  pockthlem  12712  pockthg  12713  infpnlem2  12716  1arith  12723  4sqlem9  12742  4sqlem10  12743  4sqlem11  12757  4sqlem12  12758  4sqlem13m  12759  4sqlem14  12760  4sqlem16  12762  oddennn  12796  ennnfonelemk  12804  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemrnh  12820  ennnfonelemen  12825  ennnfonelemim  12828  ctinfomlemom  12831  ctiunctlemf  12842  ssnnctlemct  12850  nninfdclemcl  12852  nninfdclemp1  12854  nninfdclemlt  12855  unbendc  12858  prdsbascl  13154  pwselbas  13159  mgmb1mgm1  13233  mgm1  13235  mgmidsssn0  13249  gsumfzval  13256  gsumress  13260  gsum0g  13261  gsumval2  13262  sgrp1  13276  sgrpidmndm  13285  ismndd  13302  prds0g  13314  mhmpropd  13331  resmhm  13352  resmhm2b  13354  gsumwsubmcl  13361  gsumwmhm  13363  isgrpd2e  13385  grpidd2  13406  isgrpinv  13419  grpinvinv  13432  grpidssd  13441  grpinvssd  13442  mulgval  13491  mulgfng  13493  mulgnegnn  13501  subg0  13549  issubg4m  13562  nsgconj  13575  1nsgtrivd  13588  eqgen  13596  eqgcpbl  13597  qus0  13604  ghmid  13618  resghm  13629  ghmnsgpreima  13638  kerf1ghm  13643  conjsubgen  13647  conjnmz  13648  imasabl  13705  rnglz  13740  rngrz  13741  qusrng  13753  issrgid  13776  srg1zr  13782  ringcl  13808  isringid  13820  ringcom  13826  ringpropd  13833  ringlz  13838  ringrz  13839  ring1  13854  opprrng  13872  opprring  13874  dvdsrcld  13892  unitcld  13903  unitmulcl  13908  unitgrp  13911  unitnegcl  13925  rhmmul  13959  isrhm2d  13960  rhmdvdsr  13970  rhmopp  13971  elrhmunit  13972  rhmunitinv  13973  subrgugrp  14035  aprsym  14079  islmodd  14088  lmod0vs  14116  lmodfopne  14121  lmodcom  14128  lssclg  14159  lspsnel5a  14205  lspsneq0b  14222  lsslsp  14224  sraring  14244  sralmod  14245  rspssp  14289  rnglidlmsgrp  14292  2idlcpblrng  14318  gsumfzfsumlem0  14381  zncrng  14440  znzrh2  14441  znzrhfo  14443  znf1o  14446  znfi  14450  znhash  14451  znidom  14452  znidomb  14453  znunit  14454  znrrg  14455  psrbaglesuppg  14467  psrelbas  14470  psrelbasfi  14471  psrgrp  14480  psr0  14481  psr1clfi  14483  mplsubgfilemcl  14494  mplsubgfileminv  14495  ntridm  14631  ntrtop  14633  ntrcls0  14636  ntr0  14639  isopn3i  14640  neiss2  14647  opnneiss  14663  topssnei  14667  cnpf2  14712  icnpimaex  14716  lmcvg  14722  iscnp4  14723  cncnp  14735  cnptopresti  14743  lmfss  14749  lmtopcnp  14755  hmeores  14820  bldisj  14906  xblss2ps  14909  xblss2  14910  blhalf  14913  blssps  14932  blss  14933  ssblex  14936  blpnfctr  14944  xmetresbl  14945  mopni2  14988  bdxmet  15006  bdbl  15008  xmetxpbl  15013  metcnpi  15020  metcnpi2  15021  tgioo  15059  rescncf  15086  mulcncflem  15112  cnopnap  15116  dedekindeulemuub  15122  dedekindeulemloc  15124  dedekindeulemlu  15126  dedekindeu  15128  dedekindicclemuub  15131  dedekindicclemloc  15133  dedekindicclemlu  15135  dedekindicclemicc  15137  dedekindicc  15138  ivthinclemlopn  15141  ivthinclemuopn  15143  ivthdec  15149  ivthreinc  15150  hovergt0  15155  dich0  15157  limcimolemlt  15169  cnplimcim  15172  cnplimclemr  15174  limccnpcntop  15180  limccnp2cntop  15182  limccoap  15183  dvfgg  15193  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvaddxxbr  15206  dvmulxxbr  15207  dvaddxx  15208  dvmulxx  15209  dviaddf  15210  dvimulf  15211  dvcoapbr  15212  dvcjbr  15213  dvcj  15214  dvrecap  15218  dvmptclx  15223  dveflem  15231  elply2  15240  plyf  15242  plyaddlem  15254  plymullem  15255  plycoeid3  15262  plyco  15264  plycj  15266  dvply1  15270  dvply2g  15271  reeff1oleme  15277  eflt  15280  sin0pilem1  15286  pilem3  15288  cosq14gt0  15337  coseq0negpitopi  15341  tangtx  15343  coskpi  15353  cosordlem  15354  cosq34lt1  15355  relogef  15369  logrpap0d  15383  rplogcl  15384  logge0  15385  logdivlti  15386  cxplt3  15425  rpabscxpbnd  15445  dvdsppwf1o  15494  fsumdvdsmul  15496  mersenne  15502  perfect1  15503  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgslem1  15510  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsvalmod  15529  lgsfcl3  15531  lgsmod  15536  lgsdirprm  15544  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem3  15573  gausslemma2dlem4  15574  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem1  15591  lgsquad2lem2  15592  lgsquad3  15594  2lgslem1c  15600  2lgsoddprm  15623  2sqlem3  15627  2sqlem4  15628  2sqlem8  15633  bj-charfunr  15783  2omap  15969  pwf1oexmid  15973  subctctexmid  15974  domomsubct  15975  pw1nct  15977  nnsf  15979  peano4nninf  15980  nninfsellemeq  15988  nnnninfex  15996  cvgcmp2nlemabs  16008  iooref1o  16010  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trirec0  16020  apdifflemf  16022  apdifflemr  16023  apdiff  16024  iswomninnlem  16025  redcwlpo  16031  redc0  16033  reap0  16034  nconstwlpolemgt0  16040  neapmkvlem  16043  ltlenmkv  16046  supfz  16047  inffz  16048