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  1854  eqtrd  2240  eleqtrd  2286  neeqtrd  2406  3netr3d  2410  rexlimd2  2623  raleqtrdv  2713  rexeqtrdv  2714  ceqsalt  2803  vtoclgft  2828  vtoclegft  2852  elrab3t  2935  eueq2dc  2953  sbceq1dd  3011  csbiedf  3142  sseqtrd  3239  3sstr3d  3245  ifbothdadc  3613  snssd  3789  dfnfc2  3882  breqdi  4074  breqtrd  4085  3brtr3d  4090  csbexga  4188  reuhypd  4536  reg2exmidlema  4600  elirr  4607  en2lp  4620  onsucuni2  4630  finds  4666  iota4  5270  iota4an  5271  funimaexglem  5376  fneu  5399  fco2  5462  fssres2  5475  fresin  5476  feu  5480  f1orescnv  5560  resdif  5566  funcocnv2  5569  f1oprg  5589  fvelrnb  5649  fimacnv  5732  f1oresrab  5768  fsn2  5777  xpsng  5778  funopsn  5785  fnressn  5793  fsnunf  5807  foeqcnvco  5882  isores1  5906  isoini2  5911  riota5f  5947  riotass2  5949  riotass  5950  ovmpodxf  6094  uchoice  6246  elopabi  6304  cnvf1o  6334  smores3  6402  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  rdgon  6495  frecabcl  6508  frecsuclem  6515  nnsucsssuc  6601  nnsucuniel  6604  erref  6663  iserd  6669  swoer  6671  swoord1  6672  swoord2  6673  erth  6689  erthi  6691  eroveu  6736  pmresg  6786  mapsn  6800  fndmeng  6926  xpen  6967  phplem4  6977  phplem4on  6990  fidifsnen  6993  dif1en  7002  dif1enen  7003  fisbth  7006  diffisn  7016  ac6sfi  7021  fimax2gtri  7024  en2eqpr  7030  unsnfidcex  7043  unsnfidcel  7044  prfidceq  7051  fiintim  7054  fidcenumlemrks  7081  elfi2  7100  elfir  7101  fiuni  7106  fifo  7108  eqsupti  7124  supisoti  7138  ordiso2  7163  casef  7216  difinfsnlem  7227  ctmlemr  7236  ctssdccl  7239  enumct  7243  nninfninc  7251  nnnninfeq  7256  nnnninfeq2  7257  enomnilem  7266  exmidomni  7270  fodjum  7274  fodjuomnilemres  7276  mkvprop  7286  enmkvlem  7289  enwomnilem  7297  nninfdcinf  7299  nninfwlpoimlemdc  7305  nninfinfwlpolem  7306  pr1or2  7328  acfun  7350  2omotaplemap  7404  exmidmotap  7408  ccfunen  7411  cc2lem  7413  dfplpq2  7502  ltanqi  7550  ltmnqi  7551  ltaddnq  7555  subhalfnqq  7562  ltbtwnnqq  7563  archnqq  7565  prarloclemarch2  7567  enq0sym  7580  enq0ref  7581  enq0tr  7582  nqnq0pi  7586  nnnq0lem1  7594  distrnq0  7607  prarloclemlt  7641  prarloclemn  7647  prarloclemcalc  7650  genplt2i  7658  addnqprllem  7675  addnqprulem  7676  addlocprlemgt  7682  appdivnq  7711  prmuloc2  7715  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemru  7760  prplnqu  7768  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemladdfu  7802  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  archrecnq  7811  archrecpr  7812  caucvgprlemk  7813  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprprlemk  7831  caucvgprprlemnkeqj  7838  caucvgprprlemnbj  7841  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemexbt  7854  caucvgprprlemexb  7855  caucvgprprlem1  7857  caucvgprprlem2  7858  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  suplocexprlemlub  7872  prsrlem1  7890  addgt0sr  7923  srpospr  7931  prsrriota  7936  caucvgsrlemgt1  7943  caucvgsrlemoffgt1  7947  caucvgsr  7950  mappsrprg  7952  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  recriota  8038  axsuploc  8180  lelttr  8196  ltletr  8197  ltnsymd  8227  lensymd  8229  cnegexlem3  8284  cnegex2  8286  addcanad  8293  addcan2ad  8294  negcon1ad  8413  negne0d  8416  negrebd  8417  subeq0d  8426  subne0ad  8429  neg11d  8430  subcand  8459  subcan2d  8460  ltadd2  8527  ltadd2dd  8530  add20  8582  ltnegcon1d  8633  ltnegcon2d  8634  lenegcon1d  8635  lenegcon2d  8636  subled  8656  lesubd  8657  ltsub23d  8658  ltsub13d  8659  ltadd1dd  8664  ltsub1dd  8665  ltsub2dd  8666  leadd1dd  8667  leadd2dd  8668  lesub1dd  8669  lesub2dd  8670  recexre  8686  apreap  8695  ltmul1a  8699  reapmul1  8703  cru  8710  apreim  8711  mulge0  8727  leltap  8733  negap0d  8739  ltleap  8740  ltapd  8746  ap0gt0  8748  ap0gt0d  8749  mulcanapad  8771  mulcanap2ad  8772  eqnegad  8842  diveqap0d  8905  diveqap1d  8906  divap1d  8909  rec11apd  8919  div11apd  8939  div2subap  8945  recgt0  8958  prodgt0  8960  lemul1a  8966  lemulge12  8975  lt2msq1  8993  lediv12a  9002  recreclt  9008  nn1suc  9090  nnnlt1  9097  nn2ge  9104  nn1gt1  9105  nnrecl  9328  nn0nlt0  9356  elnn0z  9420  nnnle0  9456  nn0negleid  9476  elz2  9479  nn0n0n1ge2b  9487  nnm1ge0  9494  nn0ge0div  9495  zextle  9499  suprzclex  9506  nn0ind-raph  9525  zindd  9526  uzneg  9702  eluzadd  9712  eluzsub  9713  uzm1  9714  uz3m2nn  9729  supminfex  9753  infregelbex  9754  nn01to3  9773  irrmulap  9804  ltrec1d  9874  lerec2d  9875  ledivdivd  9879  divge1  9880  ltmul1dd  9909  ltmul2dd  9910  ltdiv1dd  9911  lediv1dd  9912  ltdiv23d  9914  lediv23d  9915  nn0ledivnn  9924  addlelt  9925  xrlelttr  9963  xrltletr  9964  xaddass2  10027  xltadd1  10033  xlt2add  10037  ixxdisj  10060  icoshftf1o  10148  icodisj  10149  lincmb01cmp  10160  iccf1o  10161  uzsubsubfz  10204  fzdisj  10209  fzopth  10218  fznatpl1  10233  fzsuc2  10236  fzp1disj  10237  fzrev2i  10243  uzdisj  10250  fseq1p1m1  10251  fzm1  10257  fzneuz  10258  fzp1nel  10261  fzrevral  10262  fznn0sub2  10285  fz0fzdiffz0  10287  difelfzle  10291  difelfznle  10292  nn0disj  10295  fzonnsub  10328  fzodisj  10337  fzouzdisj  10339  fzoun  10340  eluzgtdifelfzo  10363  ubmelfzo  10366  fzonn0p1p1  10379  ubmelm1fzo  10392  fzostep1  10403  exfzdc  10406  subfzo0  10408  zsupcllemstep  10409  infssuzex  10413  zsupssdc  10418  qtri3or  10420  exbtwnzlemex  10429  rebtwn2z  10434  qbtwnrelemcalc  10435  qbtwnre  10436  qavgle  10438  apbtwnz  10454  flid  10464  flqwordi  10468  flqmulnn0  10479  flhalf  10482  flltdivnn0lt  10484  fldiv4p1lem1div2  10485  intfracq  10502  flqdiv  10503  flqpmodeq  10509  modqmulnn  10524  mulqaddmodid  10546  modqmuladdim  10549  modqmuladdnn0  10550  m1modge3gt1  10553  q2submod  10567  modaddmodup  10569  modqsubdir  10575  modqeqmodmin  10576  modfzo0difsn  10577  uzennn  10618  uzsinds  10626  monoord2  10668  ser3mono  10669  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemqf1o  10688  iseqf1olemqk  10689  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1olemp  10697  seqf1oglem1  10701  seqf1oglem2  10702  ser3le  10719  exp3val  10723  expnegap0  10729  expgt1  10759  ltexp2a  10773  le2sq2  10797  nnlesq  10825  qsqeqor  10832  bernneq  10842  expnbnd  10845  expnlbnd  10846  expnlbnd2  10847  expeq0d  10851  sq11d  10888  nn0ltexp2  10891  expcand  10899  nn0opthd  10904  facdiv  10920  faclbnd6  10926  facubnd  10927  facavg  10928  bcval4  10934  bcp1nk  10944  bcval5  10945  bcpasc  10948  hashennnuni  10961  isfinite4im  10974  hashnncl  10977  hashunlem  10986  fiprsshashgt1  10999  hashfzp1  11006  zfz1isolemiso  11021  seq3coll  11024  hash2en  11025  iswrdiz  11038  wrdffz  11052  ccatval21sw  11099  ccatass  11102  swrdf  11146  swrdlend  11149  ccatswrd  11161  swrdccat2  11162  pfxsuffeqwrdeq  11189  ccatpfx  11192  ccats1pfxeq  11205  cats1un  11212  wrdind  11213  wrd2ind  11214  pfxccatin12  11224  swrdccat  11226  seq3shft  11264  cjth  11272  cjdivap  11335  cjne0d  11373  cjap0d  11374  cvg1nlemcxze  11408  cvg1nlemcau  11410  cvg1nlemres  11411  recvguniq  11421  resqrexlemover  11436  resqrexlemdecn  11438  resqrexlemlo  11439  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnmsq  11443  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemglsq  11448  resqrexlemga  11449  leabs  11500  absrele  11509  nn0abscl  11511  ltabs  11513  abslt  11514  absle  11515  abstri  11530  amgm2  11544  sqr11d  11599  abs00d  11612  maxabsle  11630  maxabslemlub  11633  maxleastlt  11641  maxltsup  11644  2zsupmax  11652  minmax  11656  2zinfmin  11669  xrmaxleim  11670  xrmaxiflemlub  11674  xrmaxiflemcom  11675  xrmaxiflemval  11676  xrmaxleastlt  11682  xrmaxltsup  11684  xrmaxaddlem  11686  xrmaxadd  11687  xrminmax  11691  xrmin1inf  11693  xrmin2inf  11694  xrmineqinf  11695  climi  11713  reccn2ap  11739  climge0  11751  climle  11760  climserle  11771  climrecvg1n  11774  fz1f1o  11801  summodclem3  11806  summodclem2a  11807  summodc  11809  fisumss  11818  fsum0diaglem  11866  mptfzshft  11868  fsumrev  11869  fisum0diag2  11873  fsumlessfi  11886  fsumle  11889  fsumlt  11890  isumsplit  11917  isumrpcl  11920  expcnvap0  11928  geosergap  11932  pwm1geoserap1  11934  absgtap  11936  geolim  11937  geolim2  11938  georeclim  11939  geoisumr  11944  geoisum1c  11946  cvgratnnlembern  11949  cvgratnnlemseq  11952  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodmodclem2a  12002  prodmodc  12004  zproddc  12005  fprodntrivap  12010  fprodf1o  12014  fprodssdc  12016  fprodsplitdc  12022  fprodrev  12045  fprodmodd  12067  efcllemp  12084  ege2le3  12097  eftlcvg  12113  eftlub  12116  efltim  12124  eflegeo  12127  tanaddap  12165  sinbnd  12178  cosbnd  12179  sin01bnd  12183  cos01bnd  12184  sinltxirr  12187  sin01gt0  12188  cos01gt0  12189  cos12dec  12194  eirraplem  12203  zdvdsdc  12238  dvdstr  12254  dvdsadd2b  12266  fsumdvds  12268  dvdslelemd  12269  divconjdvds  12275  alzdvds  12280  dvdsext  12281  fzm1ndvds  12282  fzo0dvdseq  12283  3dvds  12290  zeo3  12294  even2n  12300  mod2eq1n2dvds  12305  nn0ehalf  12329  nnehalf  12330  nno  12332  nn0oddm1d2  12335  divalglemnqt  12346  divalglemex  12348  divalglemeuneg  12349  divalg2  12352  divalgmod  12353  flodddiv4t2lthalf  12365  bitsfzolem  12380  bitsfzo  12381  bitsmod  12382  bitsfi  12383  bitscmp  12384  bitsinv1lem  12387  bitsinv1  12388  dvdsbnd  12392  gcdsupex  12393  gcdsupcl  12394  gcddvds  12399  divgcdz  12407  divgcdnn  12411  gcd0id  12415  gcdneg  12418  gcd1  12423  dvdsgcdidd  12430  bezoutlemnewy  12432  bezoutlemstep  12433  bezoutlemmo  12442  bezoutlemsup  12445  dfgcd3  12446  bezout  12447  dfgcd2  12450  mulgcd  12452  sqgcd  12465  dvdssqlem  12466  bezoutr1  12469  uzwodc  12473  nninfctlemfo  12476  lcmval  12500  lcmcllem  12504  dvdslcm  12506  lcmgcdlem  12514  lcmdvds  12516  lcmgcdeq  12520  ncoprmgcdne1b  12526  mulgcddvds  12531  rpmulgcd2  12532  qredeu  12534  rpdvds  12536  prmind2  12557  nprm  12560  dvdsnprmd  12562  isprm5lem  12578  isprm5  12579  divgcdodd  12580  isprm6  12584  prmexpb  12588  pw2dvds  12603  pw2dvdseulemle  12604  oddpwdclemdc  12610  sqne2sq  12614  znege1  12615  sqrt2irraplemnn  12616  divnumden  12633  divdenle  12634  qden1elz  12642  nn0sqrtelqelz  12643  hashdvds  12658  crth  12661  phimullem  12662  eulerthlemfi  12665  eulerthlemh  12668  eulerthlemth  12669  eulerth  12670  prmdiv  12672  prmdiveq  12673  hashgcdlem  12675  dvdsfi  12676  phisum  12678  odzcllem  12680  odzdvds  12683  odzphi  12684  oddprm  12697  pythagtriplem3  12705  pythagtriplem4  12706  pythagtriplem10  12707  pythagtriplem11  12712  pythagtriplem13  12714  pythagtriplem19  12720  pcprendvds  12728  pcprendvds2  12729  pcpre1  12730  pcpremul  12731  pceulem  12732  pceu  12733  pczpre  12735  pcmul  12739  pcdiv  12740  pcqmul  12741  pcqdiv  12745  pcexp  12747  pcidlem  12761  pcneg  12763  pcdvdstr  12765  pcgcd1  12766  pc2dvds  12768  dvdsprmpweq  12773  dvdsprmpweqle  12775  pcaddlem  12777  pcadd  12778  pcadd2  12779  pcmpt  12781  fldivp1  12786  pcfaclem  12787  pcfac  12788  pcbc  12789  qexpz  12790  oddprmdvds  12792  pockthlem  12794  pockthg  12795  infpnlem2  12798  1arith  12805  4sqlem9  12824  4sqlem10  12825  4sqlem11  12839  4sqlem12  12840  4sqlem13m  12841  4sqlem14  12842  4sqlem16  12844  oddennn  12878  ennnfonelemk  12886  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemrnh  12902  ennnfonelemen  12907  ennnfonelemim  12910  ctinfomlemom  12913  ctiunctlemf  12924  ssnnctlemct  12932  nninfdclemcl  12934  nninfdclemp1  12936  nninfdclemlt  12937  unbendc  12940  prdsbascl  13236  pwselbas  13241  mgmb1mgm1  13315  mgm1  13317  mgmidsssn0  13331  gsumfzval  13338  gsumress  13342  gsum0g  13343  gsumval2  13344  sgrp1  13358  sgrpidmndm  13367  ismndd  13384  prds0g  13396  mhmpropd  13413  resmhm  13434  resmhm2b  13436  gsumwsubmcl  13443  gsumwmhm  13445  isgrpd2e  13467  grpidd2  13488  isgrpinv  13501  grpinvinv  13514  grpidssd  13523  grpinvssd  13524  mulgval  13573  mulgfng  13575  mulgnegnn  13583  subg0  13631  issubg4m  13644  nsgconj  13657  1nsgtrivd  13670  eqgen  13678  eqgcpbl  13679  qus0  13686  ghmid  13700  resghm  13711  ghmnsgpreima  13720  kerf1ghm  13725  conjsubgen  13729  conjnmz  13730  imasabl  13787  rnglz  13822  rngrz  13823  qusrng  13835  issrgid  13858  srg1zr  13864  ringcl  13890  isringid  13902  ringcom  13908  ringpropd  13915  ringlz  13920  ringrz  13921  ring1  13936  opprrng  13954  opprring  13956  dvdsrcld  13974  unitcld  13985  unitmulcl  13990  unitgrp  13993  unitnegcl  14007  rhmmul  14041  isrhm2d  14042  rhmdvdsr  14052  rhmopp  14053  elrhmunit  14054  rhmunitinv  14055  subrgugrp  14117  aprsym  14161  islmodd  14170  lmod0vs  14198  lmodfopne  14203  lmodcom  14210  lssclg  14241  lspsnel5a  14287  lspsneq0b  14304  lsslsp  14306  sraring  14326  sralmod  14327  rspssp  14371  rnglidlmsgrp  14374  2idlcpblrng  14400  gsumfzfsumlem0  14463  zncrng  14522  znzrh2  14523  znzrhfo  14525  znf1o  14528  znfi  14532  znhash  14533  znidom  14534  znidomb  14535  znunit  14536  znrrg  14537  psrbaglesuppg  14549  psrelbas  14552  psrelbasfi  14553  psrgrp  14562  psr0  14563  psr1clfi  14565  mplsubgfilemcl  14576  mplsubgfileminv  14577  ntridm  14713  ntrtop  14715  ntrcls0  14718  ntr0  14721  isopn3i  14722  neiss2  14729  opnneiss  14745  topssnei  14749  cnpf2  14794  icnpimaex  14798  lmcvg  14804  iscnp4  14805  cncnp  14817  cnptopresti  14825  lmfss  14831  lmtopcnp  14837  hmeores  14902  bldisj  14988  xblss2ps  14991  xblss2  14992  blhalf  14995  blssps  15014  blss  15015  ssblex  15018  blpnfctr  15026  xmetresbl  15027  mopni2  15070  bdxmet  15088  bdbl  15090  xmetxpbl  15095  metcnpi  15102  metcnpi2  15103  tgioo  15141  rescncf  15168  mulcncflem  15194  cnopnap  15198  dedekindeulemuub  15204  dedekindeulemloc  15206  dedekindeulemlu  15208  dedekindeu  15210  dedekindicclemuub  15213  dedekindicclemloc  15215  dedekindicclemlu  15217  dedekindicclemicc  15219  dedekindicc  15220  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthdec  15231  ivthreinc  15232  hovergt0  15237  dich0  15239  limcimolemlt  15251  cnplimcim  15254  cnplimclemr  15256  limccnpcntop  15262  limccnp2cntop  15264  limccoap  15265  dvfgg  15275  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvaddxxbr  15288  dvmulxxbr  15289  dvaddxx  15290  dvmulxx  15291  dviaddf  15292  dvimulf  15293  dvcoapbr  15294  dvcjbr  15295  dvcj  15296  dvrecap  15300  dvmptclx  15305  dveflem  15313  elply2  15322  plyf  15324  plyaddlem  15336  plymullem  15337  plycoeid3  15344  plyco  15346  plycj  15348  dvply1  15352  dvply2g  15353  reeff1oleme  15359  eflt  15362  sin0pilem1  15368  pilem3  15370  cosq14gt0  15419  coseq0negpitopi  15423  tangtx  15425  coskpi  15435  cosordlem  15436  cosq34lt1  15437  relogef  15451  logrpap0d  15465  rplogcl  15466  logge0  15467  logdivlti  15468  cxplt3  15507  rpabscxpbnd  15527  dvdsppwf1o  15576  fsumdvdsmul  15578  mersenne  15584  perfect1  15585  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgslem1  15592  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsvalmod  15611  lgsfcl3  15613  lgsmod  15618  lgsdirprm  15626  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem3  15655  gausslemma2dlem4  15656  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  lgsquad2lem2  15674  lgsquad3  15676  2lgslem1c  15682  2lgsoddprm  15705  2sqlem3  15709  2sqlem4  15710  2sqlem8  15715  lpvtx  15790  umgrnloopvv  15825  umgredgne  15854  bj-charfunr  15945  2omap  16132  pw1map  16134  pwf1oexmid  16138  subctctexmid  16139  domomsubct  16140  pw1nct  16142  nnsf  16144  peano4nninf  16145  nninfsellemeq  16153  nnnninfex  16161  cvgcmp2nlemabs  16173  iooref1o  16175  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trirec0  16185  apdifflemf  16187  apdifflemr  16188  apdiff  16189  iswomninnlem  16190  redcwlpo  16196  redc0  16198  reap0  16199  nconstwlpolemgt0  16205  neapmkvlem  16208  ltlenmkv  16211  supfz  16212  inffz  16213