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  937  mpbi2and  943  bilukdc  1396  equs5or  1830  eqtrd  2210  eleqtrd  2256  neeqtrd  2375  3netr3d  2379  rexlimd2  2592  ceqsalt  2765  vtoclgft  2789  vtoclegft  2811  elrab3t  2894  eueq2dc  2912  sbceq1dd  2970  csbiedf  3099  sseqtrd  3195  3sstr3d  3201  ifbothdadc  3568  snssd  3739  dfnfc2  3829  breqdi  4020  breqtrd  4031  3brtr3d  4036  csbexga  4133  reuhypd  4473  reg2exmidlema  4535  elirr  4542  en2lp  4555  onsucuni2  4565  finds  4601  iota4  5198  iota4an  5199  funimaexglem  5301  fneu  5322  fco2  5384  fssres2  5395  fresin  5396  feu  5400  f1orescnv  5479  resdif  5485  funcocnv2  5488  f1oprg  5507  fvelrnb  5565  fimacnv  5647  f1oresrab  5683  fsn2  5692  xpsng  5693  fnressn  5704  fsnunf  5718  foeqcnvco  5793  isores1  5817  isoini2  5822  riota5f  5857  riotass2  5859  riotass  5860  ovmpodxf  6002  elopabi  6198  cnvf1o  6228  smores3  6296  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  rdgon  6389  frecabcl  6402  frecsuclem  6409  nnsucsssuc  6495  nnsucuniel  6498  erref  6557  iserd  6563  swoer  6565  swoord1  6566  swoord2  6567  erth  6581  erthi  6583  eroveu  6628  pmresg  6678  mapsn  6692  fndmeng  6812  xpen  6847  phplem4  6857  phplem4on  6869  fidifsnen  6872  dif1en  6881  dif1enen  6882  fisbth  6885  diffisn  6895  ac6sfi  6900  fimax2gtri  6903  en2eqpr  6909  unsnfidcex  6921  unsnfidcel  6922  fiintim  6930  fidcenumlemrks  6954  elfi2  6973  elfir  6974  fiuni  6979  fifo  6981  eqsupti  6997  supisoti  7011  ordiso2  7036  casef  7089  difinfsnlem  7100  ctmlemr  7109  ctssdccl  7112  enumct  7116  nnnninfeq  7128  nnnninfeq2  7129  enomnilem  7138  exmidomni  7142  fodjum  7146  fodjuomnilemres  7148  mkvprop  7158  enmkvlem  7161  enwomnilem  7169  nninfdcinf  7171  nninfwlpoimlemdc  7177  acfun  7208  2omotaplemap  7258  exmidmotap  7262  ccfunen  7265  cc2lem  7267  dfplpq2  7355  ltanqi  7403  ltmnqi  7404  ltaddnq  7408  subhalfnqq  7415  ltbtwnnqq  7416  archnqq  7418  prarloclemarch2  7420  enq0sym  7433  enq0ref  7434  enq0tr  7435  nqnq0pi  7439  nnnq0lem1  7447  distrnq0  7460  prarloclemlt  7494  prarloclemn  7500  prarloclemcalc  7503  genplt2i  7511  addnqprllem  7528  addnqprulem  7529  addlocprlemgt  7535  appdivnq  7564  prmuloc2  7568  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemru  7613  prplnqu  7621  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemladdfu  7655  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  archrecnq  7664  archrecpr  7665  caucvgprlemk  7666  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem1  7680  caucvgprprlemk  7684  caucvgprprlemnkeqj  7691  caucvgprprlemnbj  7694  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemexbt  7707  caucvgprprlemexb  7708  caucvgprprlem1  7710  caucvgprprlem2  7711  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  suplocexprlemlub  7725  prsrlem1  7743  addgt0sr  7776  srpospr  7784  prsrriota  7789  caucvgsrlemgt1  7796  caucvgsrlemoffgt1  7800  caucvgsr  7803  mappsrprg  7805  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  recriota  7891  axsuploc  8032  lelttr  8048  ltletr  8049  ltnsymd  8079  lensymd  8081  cnegexlem3  8136  cnegex2  8138  addcanad  8145  addcan2ad  8146  negcon1ad  8265  negne0d  8268  negrebd  8269  subeq0d  8278  subne0ad  8281  neg11d  8282  subcand  8311  subcan2d  8312  ltadd2  8378  ltadd2dd  8381  add20  8433  ltnegcon1d  8484  ltnegcon2d  8485  lenegcon1d  8486  lenegcon2d  8487  subled  8507  lesubd  8508  ltsub23d  8509  ltsub13d  8510  ltadd1dd  8515  ltsub1dd  8516  ltsub2dd  8517  leadd1dd  8518  leadd2dd  8519  lesub1dd  8520  lesub2dd  8521  recexre  8537  apreap  8546  ltmul1a  8550  reapmul1  8554  cru  8561  apreim  8562  mulge0  8578  leltap  8584  negap0d  8590  ltleap  8591  ltapd  8597  ap0gt0  8599  ap0gt0d  8600  mulcanapad  8622  mulcanap2ad  8623  eqnegad  8693  diveqap0d  8756  diveqap1d  8757  divap1d  8760  rec11apd  8770  div11apd  8790  div2subap  8796  recgt0  8809  prodgt0  8811  lemul1a  8817  lemulge12  8826  lt2msq1  8844  lediv12a  8853  recreclt  8859  nn1suc  8940  nnnlt1  8947  nn2ge  8954  nn1gt1  8955  nnrecl  9176  nn0nlt0  9204  elnn0z  9268  nn0negleid  9323  elz2  9326  nn0n0n1ge2b  9334  nnm1ge0  9341  nn0ge0div  9342  zextle  9346  suprzclex  9353  nn0ind-raph  9372  zindd  9373  uzneg  9548  eluzadd  9558  eluzsub  9559  uzm1  9560  uz3m2nn  9575  supminfex  9599  infregelbex  9600  nn01to3  9619  ltrec1d  9719  lerec2d  9720  ledivdivd  9724  divge1  9725  ltmul1dd  9754  ltmul2dd  9755  ltdiv1dd  9756  lediv1dd  9757  ltdiv23d  9759  lediv23d  9760  nn0ledivnn  9769  addlelt  9770  xrlelttr  9808  xrltletr  9809  xaddass2  9872  xltadd1  9878  xlt2add  9882  ixxdisj  9905  icoshftf1o  9993  icodisj  9994  lincmb01cmp  10005  iccf1o  10006  uzsubsubfz  10049  fzdisj  10054  fzopth  10063  fznatpl1  10078  fzsuc2  10081  fzp1disj  10082  fzrev2i  10088  uzdisj  10095  fseq1p1m1  10096  fzm1  10102  fzneuz  10103  fzp1nel  10106  fzrevral  10107  fznn0sub2  10130  fz0fzdiffz0  10132  difelfzle  10136  difelfznle  10137  nn0disj  10140  fzonnsub  10171  fzodisj  10180  fzouzdisj  10182  eluzgtdifelfzo  10199  ubmelfzo  10202  fzonn0p1p1  10215  ubmelm1fzo  10228  fzostep1  10239  exfzdc  10242  subfzo0  10244  qtri3or  10245  exbtwnzlemex  10252  rebtwn2z  10257  qbtwnrelemcalc  10258  qbtwnre  10259  qavgle  10261  apbtwnz  10276  flid  10286  flqwordi  10290  flqmulnn0  10301  flhalf  10304  flltdivnn0lt  10306  fldiv4p1lem1div2  10307  intfracq  10322  flqdiv  10323  flqpmodeq  10329  modqmulnn  10344  mulqaddmodid  10366  modqmuladdim  10369  modqmuladdnn0  10370  m1modge3gt1  10373  q2submod  10387  modaddmodup  10389  modqsubdir  10395  modqeqmodmin  10396  modfzo0difsn  10397  uzennn  10438  uzsinds  10444  monoord2  10479  ser3mono  10480  iseqf1olemqcl  10488  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemqf1o  10495  iseqf1olemqk  10496  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1olemp  10504  ser3le  10520  exp3val  10524  expnegap0  10530  expgt1  10560  ltexp2a  10574  le2sq2  10598  nnlesq  10626  qsqeqor  10633  bernneq  10643  expnbnd  10646  expnlbnd  10647  expnlbnd2  10648  expeq0d  10652  sq11d  10689  nn0ltexp2  10691  expcand  10699  nn0opthd  10704  facdiv  10720  faclbnd6  10726  facubnd  10727  facavg  10728  bcval4  10734  bcp1nk  10744  bcval5  10745  bcpasc  10748  hashennnuni  10761  isfinite4im  10774  hashnncl  10777  hashunlem  10786  fiprsshashgt1  10799  hashfzp1  10806  zfz1isolemiso  10821  seq3coll  10824  seq3shft  10849  cjth  10857  cjdivap  10920  cjne0d  10958  cjap0d  10959  cvg1nlemcxze  10993  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniq  11006  resqrexlemover  11021  resqrexlemdecn  11023  resqrexlemlo  11024  resqrexlemcalc2  11026  resqrexlemcalc3  11027  resqrexlemnmsq  11028  resqrexlemnm  11029  resqrexlemcvg  11030  resqrexlemglsq  11033  resqrexlemga  11034  leabs  11085  absrele  11094  nn0abscl  11096  ltabs  11098  abslt  11099  absle  11100  abstri  11115  amgm2  11129  sqr11d  11184  abs00d  11197  maxabsle  11215  maxabslemlub  11218  maxleastlt  11226  maxltsup  11229  2zsupmax  11236  minmax  11240  2zinfmin  11253  xrmaxleim  11254  xrmaxiflemlub  11258  xrmaxiflemcom  11259  xrmaxiflemval  11260  xrmaxleastlt  11266  xrmaxltsup  11268  xrmaxaddlem  11270  xrmaxadd  11271  xrminmax  11275  xrmin1inf  11277  xrmin2inf  11278  xrmineqinf  11279  climi  11297  reccn2ap  11323  climge0  11335  climle  11344  climserle  11355  climrecvg1n  11358  fz1f1o  11385  summodclem3  11390  summodclem2a  11391  summodc  11393  fisumss  11402  fsum0diaglem  11450  mptfzshft  11452  fsumrev  11453  fisum0diag2  11457  fsumlessfi  11470  fsumle  11473  fsumlt  11474  isumsplit  11501  isumrpcl  11504  expcnvap0  11512  geosergap  11516  pwm1geoserap1  11518  absgtap  11520  geolim  11521  geolim2  11522  georeclim  11523  geoisumr  11528  geoisum1c  11530  cvgratnnlembern  11533  cvgratnnlemseq  11536  cvgratnnlemsumlt  11538  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratnn  11541  cvgratz  11542  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodmodclem2a  11586  prodmodc  11588  zproddc  11589  fprodntrivap  11594  fprodf1o  11598  fprodssdc  11600  fprodsplitdc  11606  fprodrev  11629  fprodmodd  11651  efcllemp  11668  ege2le3  11681  eftlcvg  11697  eftlub  11700  efltim  11708  eflegeo  11711  tanaddap  11749  sinbnd  11762  cosbnd  11763  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  cos01gt0  11772  cos12dec  11777  eirraplem  11786  zdvdsdc  11821  dvdstr  11837  dvdsadd2b  11849  dvdslelemd  11851  divconjdvds  11857  alzdvds  11862  dvdsext  11863  fzm1ndvds  11864  fzo0dvdseq  11865  zeo3  11875  even2n  11881  mod2eq1n2dvds  11886  nn0ehalf  11910  nnehalf  11911  nno  11913  nn0oddm1d2  11916  divalglemnqt  11927  divalglemex  11929  divalglemeuneg  11930  divalg2  11933  divalgmod  11934  flodddiv4t2lthalf  11944  zsupcllemstep  11948  infssuzex  11952  zsupssdc  11957  dvdsbnd  11959  gcdsupex  11960  gcdsupcl  11961  gcddvds  11966  divgcdz  11974  divgcdnn  11978  gcd0id  11982  gcdneg  11985  gcd1  11990  dvdsgcdidd  11997  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmo  12009  bezoutlemsup  12012  dfgcd3  12013  bezout  12014  dfgcd2  12017  mulgcd  12019  sqgcd  12032  dvdssqlem  12033  bezoutr1  12036  uzwodc  12040  lcmval  12065  lcmcllem  12069  dvdslcm  12071  lcmgcdlem  12079  lcmdvds  12081  lcmgcdeq  12085  ncoprmgcdne1b  12091  mulgcddvds  12096  rpmulgcd2  12097  qredeu  12099  rpdvds  12101  prmind2  12122  nprm  12125  dvdsnprmd  12127  isprm5lem  12143  isprm5  12144  divgcdodd  12145  isprm6  12149  prmexpb  12153  pw2dvds  12168  pw2dvdseulemle  12169  oddpwdclemdc  12175  sqne2sq  12179  znege1  12180  sqrt2irraplemnn  12181  divnumden  12198  divdenle  12199  qden1elz  12207  nn0sqrtelqelz  12208  hashdvds  12223  crth  12226  phimullem  12227  eulerthlemfi  12230  eulerthlemh  12233  eulerthlemth  12234  eulerth  12235  prmdiv  12237  prmdiveq  12238  hashgcdlem  12240  phisum  12242  odzcllem  12244  odzdvds  12247  odzphi  12248  oddprm  12261  pythagtriplem3  12269  pythagtriplem4  12270  pythagtriplem10  12271  pythagtriplem11  12276  pythagtriplem13  12278  pythagtriplem19  12284  pcprendvds  12292  pcprendvds2  12293  pcpre1  12294  pcpremul  12295  pceulem  12296  pceu  12297  pczpre  12299  pcmul  12303  pcdiv  12304  pcqmul  12305  pcqdiv  12309  pcexp  12311  pcidlem  12324  pcneg  12326  pcdvdstr  12328  pcgcd1  12329  pc2dvds  12331  dvdsprmpweq  12336  dvdsprmpweqle  12338  pcaddlem  12340  pcadd  12341  pcmpt  12343  fldivp1  12348  pcfaclem  12349  pcfac  12350  pcbc  12351  qexpz  12352  oddprmdvds  12354  pockthlem  12356  pockthg  12357  infpnlem2  12360  1arith  12367  4sqlem9  12386  4sqlem10  12387  oddennn  12395  ennnfonelemk  12403  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemrnh  12419  ennnfonelemen  12424  ennnfonelemim  12427  ctinfomlemom  12430  ctiunctlemf  12441  ssnnctlemct  12449  nninfdclemcl  12451  nninfdclemp1  12453  nninfdclemlt  12454  unbendc  12457  mgmb1mgm1  12792  mgm1  12794  mgmidsssn0  12808  sgrp1  12821  sgrpidmndm  12826  ismndd  12843  mhmpropd  12862  isgrpd2e  12901  grpidd2  12919  isgrpinv  12931  grpinvinv  12942  grpidssd  12951  grpinvssd  12952  mulgval  12991  mulgfng  12992  mulgnegnn  12998  subg0  13045  issubg4m  13058  nsgconj  13071  1nsgtrivd  13084  eqgen  13091  eqgcpbl  13092  issrgid  13169  srg1zr  13175  ringcl  13201  isringid  13213  ringcom  13219  ringpropd  13222  ringlz  13227  ringrz  13228  ring1  13241  opprring  13254  dvdsrcld  13271  unitcld  13282  unitmulcl  13287  unitgrp  13290  unitnegcl  13304  subrgugrp  13366  aprsym  13379  islmodd  13388  lmod0vs  13416  lmodfopne  13421  lmodcom  13428  lssclg  13456  ntridm  13665  ntrtop  13667  ntrcls0  13670  ntr0  13673  isopn3i  13674  neiss2  13681  opnneiss  13697  topssnei  13701  cnpf2  13746  icnpimaex  13750  lmcvg  13756  iscnp4  13757  cncnp  13769  cnptopresti  13777  lmfss  13783  lmtopcnp  13789  hmeores  13854  bldisj  13940  xblss2ps  13943  xblss2  13944  blhalf  13947  blssps  13966  blss  13967  ssblex  13970  blpnfctr  13978  xmetresbl  13979  mopni2  14022  bdxmet  14040  bdbl  14042  xmetxpbl  14047  metcnpi  14054  metcnpi2  14055  tgioo  14085  rescncf  14107  mulcncflem  14129  cnopnap  14133  dedekindeulemuub  14134  dedekindeulemloc  14136  dedekindeulemlu  14138  dedekindeu  14140  dedekindicclemuub  14143  dedekindicclemloc  14145  dedekindicclemlu  14147  dedekindicclemicc  14149  dedekindicc  14150  ivthinclemlopn  14153  ivthinclemuopn  14155  ivthdec  14161  limcimolemlt  14172  cnplimcim  14175  cnplimclemr  14177  limccnpcntop  14183  limccnp2cntop  14185  limccoap  14186  dvfgg  14196  dvidlemap  14199  dvaddxxbr  14204  dvmulxxbr  14205  dvaddxx  14206  dvmulxx  14207  dviaddf  14208  dvimulf  14209  dvcoapbr  14210  dvcjbr  14211  dvcj  14212  dvrecap  14216  dvmptclx  14219  dveflem  14226  reeff1oleme  14232  eflt  14235  sin0pilem1  14241  pilem3  14243  cosq14gt0  14292  coseq0negpitopi  14296  tangtx  14298  coskpi  14308  cosordlem  14309  cosq34lt1  14310  relogef  14324  logrpap0d  14338  rplogcl  14339  logge0  14340  logdivlti  14341  cxplt3  14379  rpabscxpbnd  14398  lgslem1  14440  lgsval  14444  lgsfvalg  14445  lgsval2lem  14450  lgsvalmod  14459  lgsfcl3  14461  lgsmod  14466  lgsdirprm  14474  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  2sqlem3  14503  2sqlem4  14504  2sqlem8  14509  bj-charfunr  14601  pwf1oexmid  14788  subctctexmid  14789  pw1nct  14791  nnsf  14793  peano4nninf  14794  nninfsellemeq  14802  cvgcmp2nlemabs  14819  iooref1o  14821  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  trirec0  14831  apdifflemf  14833  apdifflemr  14834  apdiff  14835  iswomninnlem  14836  redcwlpo  14842  redc0  14844  reap0  14845  nconstwlpolemgt0  14850  neapmkvlem  14853  ltlenmkv  14856  supfz  14857  inffz  14858