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  927  mpbi2and  933  bilukdc  1386  equs5or  1818  eqtrd  2198  eleqtrd  2244  neeqtrd  2363  3netr3d  2367  rexlimd2  2580  ceqsalt  2751  vtoclgft  2775  vtoclegft  2797  elrab3t  2880  eueq2dc  2898  sbceq1dd  2956  csbiedf  3084  sseqtrd  3179  3sstr3d  3185  ifbothdadc  3550  snssd  3717  dfnfc2  3806  breqdi  3996  breqtrd  4007  3brtr3d  4012  csbexga  4109  reuhypd  4448  reg2exmidlema  4510  elirr  4517  en2lp  4530  onsucuni2  4540  finds  4576  iota4  5170  iota4an  5171  funimaexglem  5270  fneu  5291  fco2  5353  fssres2  5364  fresin  5365  feu  5369  f1orescnv  5447  resdif  5453  funcocnv2  5456  f1oprg  5475  fvelrnb  5533  fimacnv  5613  f1oresrab  5649  fsn2  5658  xpsng  5659  fnressn  5670  fsnunf  5684  foeqcnvco  5757  isores1  5781  isoini2  5786  riota5f  5821  riotass2  5823  riotass  5824  ovmpodxf  5963  elopabi  6160  cnvf1o  6189  smores3  6257  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  rdgon  6350  frecabcl  6363  frecsuclem  6370  nnsucsssuc  6456  nnsucuniel  6459  erref  6517  iserd  6523  swoer  6525  swoord1  6526  swoord2  6527  erth  6541  erthi  6543  eroveu  6588  pmresg  6638  mapsn  6652  fndmeng  6772  xpen  6807  phplem4  6817  phplem4on  6829  fidifsnen  6832  dif1en  6841  dif1enen  6842  fisbth  6845  diffisn  6855  ac6sfi  6860  fimax2gtri  6863  en2eqpr  6869  unsnfidcex  6881  unsnfidcel  6882  fiintim  6890  fidcenumlemrks  6914  elfi2  6933  elfir  6934  fiuni  6939  fifo  6941  eqsupti  6957  supisoti  6971  ordiso2  6996  casef  7049  difinfsnlem  7060  ctmlemr  7069  ctssdccl  7072  enumct  7076  nnnninfeq  7088  nnnninfeq2  7089  enomnilem  7098  exmidomni  7102  fodjum  7106  fodjuomnilemres  7108  mkvprop  7118  enmkvlem  7121  enwomnilem  7129  acfun  7159  ccfunen  7201  cc2lem  7203  dfplpq2  7291  ltanqi  7339  ltmnqi  7340  ltaddnq  7344  subhalfnqq  7351  ltbtwnnqq  7352  archnqq  7354  prarloclemarch2  7356  enq0sym  7369  enq0ref  7370  enq0tr  7371  nqnq0pi  7375  nnnq0lem1  7383  distrnq0  7396  prarloclemlt  7430  prarloclemn  7436  prarloclemcalc  7439  genplt2i  7447  addnqprllem  7464  addnqprulem  7465  addlocprlemgt  7471  appdivnq  7500  prmuloc2  7504  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemru  7549  prplnqu  7557  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemladdfu  7591  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  archrecnq  7600  archrecpr  7601  caucvgprlemk  7602  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprprlemk  7620  caucvgprprlemnkeqj  7627  caucvgprprlemnbj  7630  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemexbt  7643  caucvgprprlemexb  7644  caucvgprprlem1  7646  caucvgprprlem2  7647  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  prsrlem1  7679  addgt0sr  7712  srpospr  7720  prsrriota  7725  caucvgsrlemgt1  7732  caucvgsrlemoffgt1  7736  caucvgsr  7739  mappsrprg  7741  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  recriota  7827  axsuploc  7967  lelttr  7983  ltletr  7984  ltnsymd  8014  lensymd  8016  cnegexlem3  8071  cnegex2  8073  addcanad  8080  addcan2ad  8081  negcon1ad  8200  negne0d  8203  negrebd  8204  subeq0d  8213  subne0ad  8216  neg11d  8217  subcand  8246  subcan2d  8247  ltadd2  8313  ltadd2dd  8316  add20  8368  ltnegcon1d  8419  ltnegcon2d  8420  lenegcon1d  8421  lenegcon2d  8422  subled  8442  lesubd  8443  ltsub23d  8444  ltsub13d  8445  ltadd1dd  8450  ltsub1dd  8451  ltsub2dd  8452  leadd1dd  8453  leadd2dd  8454  lesub1dd  8455  lesub2dd  8456  recexre  8472  apreap  8481  ltmul1a  8485  reapmul1  8489  cru  8496  apreim  8497  mulge0  8513  leltap  8519  negap0d  8525  ltleap  8526  ltapd  8532  ap0gt0  8534  ap0gt0d  8535  mulcanapad  8556  mulcanap2ad  8557  eqnegad  8626  diveqap0d  8689  diveqap1d  8690  divap1d  8693  rec11apd  8703  div11apd  8723  div2subap  8729  recgt0  8741  prodgt0  8743  lemul1a  8749  lemulge12  8758  lt2msq1  8776  lediv12a  8785  recreclt  8791  nn1suc  8872  nnnlt1  8879  nn2ge  8886  nn1gt1  8887  nnrecl  9108  nn0nlt0  9136  elnn0z  9200  nn0negleid  9255  elz2  9258  nn0n0n1ge2b  9266  nnm1ge0  9273  nn0ge0div  9274  zextle  9278  suprzclex  9285  nn0ind-raph  9304  zindd  9305  uzneg  9480  eluzadd  9490  eluzsub  9491  uzm1  9492  uz3m2nn  9507  supminfex  9531  infregelbex  9532  nn01to3  9551  ltrec1d  9649  lerec2d  9650  ledivdivd  9654  divge1  9655  ltmul1dd  9684  ltmul2dd  9685  ltdiv1dd  9686  lediv1dd  9687  ltdiv23d  9689  lediv23d  9690  nn0ledivnn  9699  addlelt  9700  xrlelttr  9738  xrltletr  9739  xaddass2  9802  xltadd1  9808  xlt2add  9812  ixxdisj  9835  icoshftf1o  9923  icodisj  9924  lincmb01cmp  9935  iccf1o  9936  uzsubsubfz  9978  fzdisj  9983  fzopth  9992  fznatpl1  10007  fzsuc2  10010  fzp1disj  10011  fzrev2i  10017  uzdisj  10024  fseq1p1m1  10025  fzm1  10031  fzneuz  10032  fzp1nel  10035  fzrevral  10036  fznn0sub2  10059  fz0fzdiffz0  10061  difelfzle  10065  difelfznle  10066  nn0disj  10069  fzonnsub  10100  fzodisj  10109  fzouzdisj  10111  eluzgtdifelfzo  10128  ubmelfzo  10131  fzonn0p1p1  10144  ubmelm1fzo  10157  fzostep1  10168  exfzdc  10171  subfzo0  10173  qtri3or  10174  exbtwnzlemex  10181  rebtwn2z  10186  qbtwnrelemcalc  10187  qbtwnre  10188  qavgle  10190  apbtwnz  10205  flid  10215  flqwordi  10219  flqmulnn0  10230  flhalf  10233  flltdivnn0lt  10235  fldiv4p1lem1div2  10236  intfracq  10251  flqdiv  10252  flqpmodeq  10258  modqmulnn  10273  mulqaddmodid  10295  modqmuladdim  10298  modqmuladdnn0  10299  m1modge3gt1  10302  q2submod  10316  modaddmodup  10318  modqsubdir  10324  modqeqmodmin  10325  modfzo0difsn  10326  uzennn  10367  uzsinds  10373  monoord2  10408  ser3mono  10409  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemab  10420  iseqf1olemqf1o  10424  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemp  10433  ser3le  10449  exp3val  10453  expnegap0  10459  expgt1  10489  ltexp2a  10503  le2sq2  10526  nnlesq  10554  qsqeqor  10561  bernneq  10571  expnbnd  10574  expnlbnd  10575  expnlbnd2  10576  expeq0d  10580  sq11d  10617  nn0ltexp2  10619  expcand  10626  nn0opthd  10631  facdiv  10647  faclbnd6  10653  facubnd  10654  facavg  10655  bcval4  10661  bcp1nk  10671  bcval5  10672  bcpasc  10675  hashennnuni  10688  focdmex  10696  isfinite4im  10702  hashnncl  10705  hashunlem  10713  fiprsshashgt1  10726  hashfzp1  10733  zfz1isolemiso  10748  seq3coll  10751  seq3shft  10776  cjth  10784  cjdivap  10847  cjne0d  10885  cjap0d  10886  cvg1nlemcxze  10920  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniq  10933  resqrexlemover  10948  resqrexlemdecn  10950  resqrexlemlo  10951  resqrexlemcalc2  10953  resqrexlemcalc3  10954  resqrexlemnmsq  10955  resqrexlemnm  10956  resqrexlemcvg  10957  resqrexlemglsq  10960  resqrexlemga  10961  leabs  11012  absrele  11021  nn0abscl  11023  ltabs  11025  abslt  11026  absle  11027  abstri  11042  amgm2  11056  sqr11d  11111  abs00d  11124  maxabsle  11142  maxabslemlub  11145  maxleastlt  11153  maxltsup  11156  2zsupmax  11163  minmax  11167  2zinfmin  11180  xrmaxleim  11181  xrmaxiflemlub  11185  xrmaxiflemcom  11186  xrmaxiflemval  11187  xrmaxleastlt  11193  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  xrminmax  11202  xrmin1inf  11204  xrmin2inf  11205  xrmineqinf  11206  climi  11224  reccn2ap  11250  climge0  11262  climle  11271  climserle  11282  climrecvg1n  11285  fz1f1o  11312  summodclem3  11317  summodclem2a  11318  summodc  11320  fisumss  11329  fsum0diaglem  11377  mptfzshft  11379  fsumrev  11380  fisum0diag2  11384  fsumlessfi  11397  fsumle  11400  fsumlt  11401  isumsplit  11428  isumrpcl  11431  expcnvap0  11439  geosergap  11443  pwm1geoserap1  11445  absgtap  11447  geolim  11448  geolim2  11449  georeclim  11450  geoisumr  11455  geoisum1c  11457  cvgratnnlembern  11460  cvgratnnlemseq  11463  cvgratnnlemsumlt  11465  cvgratnnlemfm  11466  cvgratnnlemrate  11467  cvgratnn  11468  cvgratz  11469  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodmodclem2a  11513  prodmodc  11515  zproddc  11516  fprodntrivap  11521  fprodf1o  11525  fprodssdc  11527  fprodsplitdc  11533  fprodrev  11556  fprodmodd  11578  efcllemp  11595  ege2le3  11608  eftlcvg  11624  eftlub  11627  efltim  11635  eflegeo  11638  tanaddap  11676  sinbnd  11689  cosbnd  11690  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  cos01gt0  11699  cos12dec  11704  eirraplem  11713  zdvdsdc  11748  dvdstr  11764  dvdsadd2b  11776  dvdslelemd  11777  divconjdvds  11783  alzdvds  11788  dvdsext  11789  fzm1ndvds  11790  fzo0dvdseq  11791  zeo3  11801  even2n  11807  mod2eq1n2dvds  11812  nn0ehalf  11836  nnehalf  11837  nno  11839  nn0oddm1d2  11842  divalglemnqt  11853  divalglemex  11855  divalglemeuneg  11856  divalg2  11859  divalgmod  11860  flodddiv4t2lthalf  11870  zsupcllemstep  11874  infssuzex  11878  zsupssdc  11883  dvdsbnd  11885  gcdsupex  11886  gcdsupcl  11887  gcddvds  11892  divgcdz  11900  divgcdnn  11904  gcd0id  11908  gcdneg  11911  gcd1  11916  dvdsgcdidd  11923  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemmo  11935  bezoutlemsup  11938  dfgcd3  11939  bezout  11940  dfgcd2  11943  mulgcd  11945  sqgcd  11958  dvdssqlem  11959  bezoutr1  11962  uzwodc  11966  lcmval  11991  lcmcllem  11995  dvdslcm  11997  lcmgcdlem  12005  lcmdvds  12007  lcmgcdeq  12011  ncoprmgcdne1b  12017  mulgcddvds  12022  rpmulgcd2  12023  qredeu  12025  rpdvds  12027  prmind2  12048  nprm  12051  dvdsnprmd  12053  isprm5lem  12069  isprm5  12070  divgcdodd  12071  isprm6  12075  prmexpb  12079  pw2dvds  12094  pw2dvdseulemle  12095  oddpwdclemdc  12101  sqne2sq  12105  znege1  12106  sqrt2irraplemnn  12107  divnumden  12124  divdenle  12125  qden1elz  12133  nn0sqrtelqelz  12134  hashdvds  12149  crth  12152  phimullem  12153  eulerthlemfi  12156  eulerthlemh  12159  eulerthlemth  12160  eulerth  12161  prmdiv  12163  prmdiveq  12164  hashgcdlem  12166  phisum  12168  odzcllem  12170  odzdvds  12173  odzphi  12174  oddprm  12187  pythagtriplem3  12195  pythagtriplem4  12196  pythagtriplem10  12197  pythagtriplem11  12202  pythagtriplem13  12204  pythagtriplem19  12210  pcprendvds  12218  pcprendvds2  12219  pcpre1  12220  pcpremul  12221  pceulem  12222  pceu  12223  pczpre  12225  pcmul  12229  pcdiv  12230  pcqmul  12231  pcqdiv  12235  pcexp  12237  pcidlem  12250  pcneg  12252  pcdvdstr  12254  pcgcd1  12255  pc2dvds  12257  dvdsprmpweq  12262  dvdsprmpweqle  12264  pcaddlem  12266  pcadd  12267  pcmpt  12269  fldivp1  12274  pcfaclem  12275  pcfac  12276  pcbc  12277  qexpz  12278  oddprmdvds  12280  pockthlem  12282  pockthg  12283  infpnlem2  12286  1arith  12293  4sqlem9  12312  4sqlem10  12313  oddennn  12321  ennnfonelemk  12329  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemrnh  12345  ennnfonelemen  12350  ennnfonelemim  12353  ctinfomlemom  12356  ctiunctlemf  12367  ssnnctlemct  12375  nninfdclemcl  12377  nninfdclemp1  12379  nninfdclemlt  12380  unbendc  12383  ntridm  12726  ntrtop  12728  ntrcls0  12731  ntr0  12734  isopn3i  12735  neiss2  12742  opnneiss  12758  topssnei  12762  cnpf2  12807  icnpimaex  12811  lmcvg  12817  iscnp4  12818  cncnp  12830  cnptopresti  12838  lmfss  12844  lmtopcnp  12850  hmeores  12915  bldisj  13001  xblss2ps  13004  xblss2  13005  blhalf  13008  blssps  13027  blss  13028  ssblex  13031  blpnfctr  13039  xmetresbl  13040  mopni2  13083  bdxmet  13101  bdbl  13103  xmetxpbl  13108  metcnpi  13115  metcnpi2  13116  tgioo  13146  rescncf  13168  mulcncflem  13190  cnopnap  13194  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeu  13201  dedekindicclemuub  13204  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemicc  13210  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthdec  13222  limcimolemlt  13233  cnplimcim  13236  cnplimclemr  13238  limccnpcntop  13244  limccnp2cntop  13246  limccoap  13247  dvfgg  13257  dvidlemap  13260  dvaddxxbr  13265  dvmulxxbr  13266  dvaddxx  13267  dvmulxx  13268  dviaddf  13269  dvimulf  13270  dvcoapbr  13271  dvcjbr  13272  dvcj  13273  dvrecap  13277  dvmptclx  13280  dveflem  13287  reeff1oleme  13293  eflt  13296  sin0pilem1  13302  pilem3  13304  cosq14gt0  13353  coseq0negpitopi  13357  tangtx  13359  coskpi  13369  cosordlem  13370  cosq34lt1  13371  relogef  13385  logrpap0d  13399  rplogcl  13400  logge0  13401  logdivlti  13402  cxplt3  13440  rpabscxpbnd  13459  lgslem1  13501  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsvalmod  13520  lgsfcl3  13522  lgsmod  13527  lgsdirprm  13535  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  2sqlem3  13553  2sqlem4  13554  2sqlem8  13559  bj-charfunr  13652  pwf1oexmid  13839  subctctexmid  13841  pw1nct  13843  nnsf  13845  peano4nninf  13846  nninfsellemeq  13854  cvgcmp2nlemabs  13871  iooref1o  13873  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  trirec0  13883  apdifflemf  13885  apdifflemr  13886  apdiff  13887  iswomninnlem  13888  redcwlpo  13894  redc0  13896  reap0  13897  nconstwlpolemgt0  13902  neapmkvlem  13905  supfz  13907  inffz  13908