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  939  mpbi2and  945  bilukdc  1407  equs5or  1844  eqtrd  2229  eleqtrd  2275  neeqtrd  2395  3netr3d  2399  rexlimd2  2612  raleqtrdv  2701  rexeqtrdv  2702  ceqsalt  2789  vtoclgft  2814  vtoclegft  2836  elrab3t  2919  eueq2dc  2937  sbceq1dd  2995  csbiedf  3125  sseqtrd  3221  3sstr3d  3227  ifbothdadc  3593  snssd  3767  dfnfc2  3857  breqdi  4048  breqtrd  4059  3brtr3d  4064  csbexga  4161  reuhypd  4506  reg2exmidlema  4570  elirr  4577  en2lp  4590  onsucuni2  4600  finds  4636  iota4  5238  iota4an  5239  funimaexglem  5341  fneu  5362  fco2  5424  fssres2  5435  fresin  5436  feu  5440  f1orescnv  5520  resdif  5526  funcocnv2  5529  f1oprg  5548  fvelrnb  5608  fimacnv  5691  f1oresrab  5727  fsn2  5736  xpsng  5737  fnressn  5748  fsnunf  5762  foeqcnvco  5837  isores1  5861  isoini2  5866  riota5f  5902  riotass2  5904  riotass  5905  ovmpodxf  6048  uchoice  6195  elopabi  6253  cnvf1o  6283  smores3  6351  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  rdgon  6444  frecabcl  6457  frecsuclem  6464  nnsucsssuc  6550  nnsucuniel  6553  erref  6612  iserd  6618  swoer  6620  swoord1  6621  swoord2  6622  erth  6638  erthi  6640  eroveu  6685  pmresg  6735  mapsn  6749  fndmeng  6869  xpen  6906  phplem4  6916  phplem4on  6928  fidifsnen  6931  dif1en  6940  dif1enen  6941  fisbth  6944  diffisn  6954  ac6sfi  6959  fimax2gtri  6962  en2eqpr  6968  unsnfidcex  6981  unsnfidcel  6982  prfidceq  6989  fiintim  6992  fidcenumlemrks  7019  elfi2  7038  elfir  7039  fiuni  7044  fifo  7046  eqsupti  7062  supisoti  7076  ordiso2  7101  casef  7154  difinfsnlem  7165  ctmlemr  7174  ctssdccl  7177  enumct  7181  nninfninc  7189  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  exmidomni  7208  fodjum  7212  fodjuomnilemres  7214  mkvprop  7224  enmkvlem  7227  enwomnilem  7235  nninfdcinf  7237  nninfwlpoimlemdc  7243  acfun  7274  2omotaplemap  7324  exmidmotap  7328  ccfunen  7331  cc2lem  7333  dfplpq2  7421  ltanqi  7469  ltmnqi  7470  ltaddnq  7474  subhalfnqq  7481  ltbtwnnqq  7482  archnqq  7484  prarloclemarch2  7486  enq0sym  7499  enq0ref  7500  enq0tr  7501  nqnq0pi  7505  nnnq0lem1  7513  distrnq0  7526  prarloclemlt  7560  prarloclemn  7566  prarloclemcalc  7569  genplt2i  7577  addnqprllem  7594  addnqprulem  7595  addlocprlemgt  7601  appdivnq  7630  prmuloc2  7634  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemru  7679  prplnqu  7687  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemladdfu  7721  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  archrecnq  7730  archrecpr  7731  caucvgprlemk  7732  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprprlemk  7750  caucvgprprlemnkeqj  7757  caucvgprprlemnbj  7760  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  caucvgprprlem1  7776  caucvgprprlem2  7777  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  prsrlem1  7809  addgt0sr  7842  srpospr  7850  prsrriota  7855  caucvgsrlemgt1  7862  caucvgsrlemoffgt1  7866  caucvgsr  7869  mappsrprg  7871  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  recriota  7957  axsuploc  8099  lelttr  8115  ltletr  8116  ltnsymd  8146  lensymd  8148  cnegexlem3  8203  cnegex2  8205  addcanad  8212  addcan2ad  8213  negcon1ad  8332  negne0d  8335  negrebd  8336  subeq0d  8345  subne0ad  8348  neg11d  8349  subcand  8378  subcan2d  8379  ltadd2  8446  ltadd2dd  8449  add20  8501  ltnegcon1d  8552  ltnegcon2d  8553  lenegcon1d  8554  lenegcon2d  8555  subled  8575  lesubd  8576  ltsub23d  8577  ltsub13d  8578  ltadd1dd  8583  ltsub1dd  8584  ltsub2dd  8585  leadd1dd  8586  leadd2dd  8587  lesub1dd  8588  lesub2dd  8589  recexre  8605  apreap  8614  ltmul1a  8618  reapmul1  8622  cru  8629  apreim  8630  mulge0  8646  leltap  8652  negap0d  8658  ltleap  8659  ltapd  8665  ap0gt0  8667  ap0gt0d  8668  mulcanapad  8690  mulcanap2ad  8691  eqnegad  8761  diveqap0d  8824  diveqap1d  8825  divap1d  8828  rec11apd  8838  div11apd  8858  div2subap  8864  recgt0  8877  prodgt0  8879  lemul1a  8885  lemulge12  8894  lt2msq1  8912  lediv12a  8921  recreclt  8927  nn1suc  9009  nnnlt1  9016  nn2ge  9023  nn1gt1  9024  nnrecl  9247  nn0nlt0  9275  elnn0z  9339  nn0negleid  9394  elz2  9397  nn0n0n1ge2b  9405  nnm1ge0  9412  nn0ge0div  9413  zextle  9417  suprzclex  9424  nn0ind-raph  9443  zindd  9444  uzneg  9620  eluzadd  9630  eluzsub  9631  uzm1  9632  uz3m2nn  9647  supminfex  9671  infregelbex  9672  nn01to3  9691  irrmulap  9722  ltrec1d  9792  lerec2d  9793  ledivdivd  9797  divge1  9798  ltmul1dd  9827  ltmul2dd  9828  ltdiv1dd  9829  lediv1dd  9830  ltdiv23d  9832  lediv23d  9833  nn0ledivnn  9842  addlelt  9843  xrlelttr  9881  xrltletr  9882  xaddass2  9945  xltadd1  9951  xlt2add  9955  ixxdisj  9978  icoshftf1o  10066  icodisj  10067  lincmb01cmp  10078  iccf1o  10079  uzsubsubfz  10122  fzdisj  10127  fzopth  10136  fznatpl1  10151  fzsuc2  10154  fzp1disj  10155  fzrev2i  10161  uzdisj  10168  fseq1p1m1  10169  fzm1  10175  fzneuz  10176  fzp1nel  10179  fzrevral  10180  fznn0sub2  10203  fz0fzdiffz0  10205  difelfzle  10209  difelfznle  10210  nn0disj  10213  fzonnsub  10245  fzodisj  10254  fzouzdisj  10256  eluzgtdifelfzo  10273  ubmelfzo  10276  fzonn0p1p1  10289  ubmelm1fzo  10302  fzostep1  10313  exfzdc  10316  subfzo0  10318  zsupcllemstep  10319  infssuzex  10323  zsupssdc  10328  qtri3or  10330  exbtwnzlemex  10339  rebtwn2z  10344  qbtwnrelemcalc  10345  qbtwnre  10346  qavgle  10348  apbtwnz  10364  flid  10374  flqwordi  10378  flqmulnn0  10389  flhalf  10392  flltdivnn0lt  10394  fldiv4p1lem1div2  10395  intfracq  10412  flqdiv  10413  flqpmodeq  10419  modqmulnn  10434  mulqaddmodid  10456  modqmuladdim  10459  modqmuladdnn0  10460  m1modge3gt1  10463  q2submod  10477  modaddmodup  10479  modqsubdir  10485  modqeqmodmin  10486  modfzo0difsn  10487  uzennn  10528  uzsinds  10536  monoord2  10578  ser3mono  10579  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemqf1o  10598  iseqf1olemqk  10599  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemp  10607  seqf1oglem1  10611  seqf1oglem2  10612  ser3le  10629  exp3val  10633  expnegap0  10639  expgt1  10669  ltexp2a  10683  le2sq2  10707  nnlesq  10735  qsqeqor  10742  bernneq  10752  expnbnd  10755  expnlbnd  10756  expnlbnd2  10757  expeq0d  10761  sq11d  10798  nn0ltexp2  10801  expcand  10809  nn0opthd  10814  facdiv  10830  faclbnd6  10836  facubnd  10837  facavg  10838  bcval4  10844  bcp1nk  10854  bcval5  10855  bcpasc  10858  hashennnuni  10871  isfinite4im  10884  hashnncl  10887  hashunlem  10896  fiprsshashgt1  10909  hashfzp1  10916  zfz1isolemiso  10931  seq3coll  10934  iswrdiz  10942  wrdffz  10956  seq3shft  11003  cjth  11011  cjdivap  11074  cjne0d  11112  cjap0d  11113  cvg1nlemcxze  11147  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniq  11160  resqrexlemover  11175  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemnmsq  11182  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemglsq  11187  resqrexlemga  11188  leabs  11239  absrele  11248  nn0abscl  11250  ltabs  11252  abslt  11253  absle  11254  abstri  11269  amgm2  11283  sqr11d  11338  abs00d  11351  maxabsle  11369  maxabslemlub  11372  maxleastlt  11380  maxltsup  11383  2zsupmax  11391  minmax  11395  2zinfmin  11408  xrmaxleim  11409  xrmaxiflemlub  11413  xrmaxiflemcom  11414  xrmaxiflemval  11415  xrmaxleastlt  11421  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  xrminmax  11430  xrmin1inf  11432  xrmin2inf  11433  xrmineqinf  11434  climi  11452  reccn2ap  11478  climge0  11490  climle  11499  climserle  11510  climrecvg1n  11513  fz1f1o  11540  summodclem3  11545  summodclem2a  11546  summodc  11548  fisumss  11557  fsum0diaglem  11605  mptfzshft  11607  fsumrev  11608  fisum0diag2  11612  fsumlessfi  11625  fsumle  11628  fsumlt  11629  isumsplit  11656  isumrpcl  11659  expcnvap0  11667  geosergap  11671  pwm1geoserap1  11673  absgtap  11675  geolim  11676  geolim2  11677  georeclim  11678  geoisumr  11683  geoisum1c  11685  cvgratnnlembern  11688  cvgratnnlemseq  11691  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  cvgratz  11697  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodmodclem2a  11741  prodmodc  11743  zproddc  11744  fprodntrivap  11749  fprodf1o  11753  fprodssdc  11755  fprodsplitdc  11761  fprodrev  11784  fprodmodd  11806  efcllemp  11823  ege2le3  11836  eftlcvg  11852  eftlub  11855  efltim  11863  eflegeo  11866  tanaddap  11904  sinbnd  11917  cosbnd  11918  sin01bnd  11922  cos01bnd  11923  sinltxirr  11926  sin01gt0  11927  cos01gt0  11928  cos12dec  11933  eirraplem  11942  zdvdsdc  11977  dvdstr  11993  dvdsadd2b  12005  fsumdvds  12007  dvdslelemd  12008  divconjdvds  12014  alzdvds  12019  dvdsext  12020  fzm1ndvds  12021  fzo0dvdseq  12022  3dvds  12029  zeo3  12033  even2n  12039  mod2eq1n2dvds  12044  nn0ehalf  12068  nnehalf  12069  nno  12071  nn0oddm1d2  12074  divalglemnqt  12085  divalglemex  12087  divalglemeuneg  12088  divalg2  12091  divalgmod  12092  flodddiv4t2lthalf  12104  bitsfzolem  12118  bitsfzo  12119  dvdsbnd  12123  gcdsupex  12124  gcdsupcl  12125  gcddvds  12130  divgcdz  12138  divgcdnn  12142  gcd0id  12146  gcdneg  12149  gcd1  12154  dvdsgcdidd  12161  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmo  12173  bezoutlemsup  12176  dfgcd3  12177  bezout  12178  dfgcd2  12181  mulgcd  12183  sqgcd  12196  dvdssqlem  12197  bezoutr1  12200  uzwodc  12204  nninfctlemfo  12207  lcmval  12231  lcmcllem  12235  dvdslcm  12237  lcmgcdlem  12245  lcmdvds  12247  lcmgcdeq  12251  ncoprmgcdne1b  12257  mulgcddvds  12262  rpmulgcd2  12263  qredeu  12265  rpdvds  12267  prmind2  12288  nprm  12291  dvdsnprmd  12293  isprm5lem  12309  isprm5  12310  divgcdodd  12311  isprm6  12315  prmexpb  12319  pw2dvds  12334  pw2dvdseulemle  12335  oddpwdclemdc  12341  sqne2sq  12345  znege1  12346  sqrt2irraplemnn  12347  divnumden  12364  divdenle  12365  qden1elz  12373  nn0sqrtelqelz  12374  hashdvds  12389  crth  12392  phimullem  12393  eulerthlemfi  12396  eulerthlemh  12399  eulerthlemth  12400  eulerth  12401  prmdiv  12403  prmdiveq  12404  hashgcdlem  12406  dvdsfi  12407  phisum  12409  odzcllem  12411  odzdvds  12414  odzphi  12415  oddprm  12428  pythagtriplem3  12436  pythagtriplem4  12437  pythagtriplem10  12438  pythagtriplem11  12443  pythagtriplem13  12445  pythagtriplem19  12451  pcprendvds  12459  pcprendvds2  12460  pcpre1  12461  pcpremul  12462  pceulem  12463  pceu  12464  pczpre  12466  pcmul  12470  pcdiv  12471  pcqmul  12472  pcqdiv  12476  pcexp  12478  pcidlem  12492  pcneg  12494  pcdvdstr  12496  pcgcd1  12497  pc2dvds  12499  dvdsprmpweq  12504  dvdsprmpweqle  12506  pcaddlem  12508  pcadd  12509  pcadd2  12510  pcmpt  12512  fldivp1  12517  pcfaclem  12518  pcfac  12519  pcbc  12520  qexpz  12521  oddprmdvds  12523  pockthlem  12525  pockthg  12526  infpnlem2  12529  1arith  12536  4sqlem9  12555  4sqlem10  12556  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem14  12573  4sqlem16  12575  oddennn  12609  ennnfonelemk  12617  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemrnh  12633  ennnfonelemen  12638  ennnfonelemim  12641  ctinfomlemom  12644  ctiunctlemf  12655  ssnnctlemct  12663  nninfdclemcl  12665  nninfdclemp1  12667  nninfdclemlt  12668  unbendc  12671  mgmb1mgm1  13011  mgm1  13013  mgmidsssn0  13027  gsumfzval  13034  gsumress  13038  gsum0g  13039  gsumval2  13040  sgrp1  13054  sgrpidmndm  13061  ismndd  13078  mhmpropd  13098  resmhm  13119  resmhm2b  13121  gsumwsubmcl  13128  gsumwmhm  13130  isgrpd2e  13152  grpidd2  13173  isgrpinv  13186  grpinvinv  13199  grpidssd  13208  grpinvssd  13209  mulgval  13252  mulgfng  13254  mulgnegnn  13262  subg0  13310  issubg4m  13323  nsgconj  13336  1nsgtrivd  13349  eqgen  13357  eqgcpbl  13358  qus0  13365  ghmid  13379  resghm  13390  ghmnsgpreima  13399  kerf1ghm  13404  conjsubgen  13408  conjnmz  13409  imasabl  13466  rnglz  13501  rngrz  13502  qusrng  13514  issrgid  13537  srg1zr  13543  ringcl  13569  isringid  13581  ringcom  13587  ringpropd  13594  ringlz  13599  ringrz  13600  ring1  13615  opprrng  13633  opprring  13635  dvdsrcld  13653  unitcld  13664  unitmulcl  13669  unitgrp  13672  unitnegcl  13686  rhmmul  13720  isrhm2d  13721  rhmdvdsr  13731  rhmopp  13732  elrhmunit  13733  rhmunitinv  13734  subrgugrp  13796  aprsym  13840  islmodd  13849  lmod0vs  13877  lmodfopne  13882  lmodcom  13889  lssclg  13920  lspsnel5a  13966  lspsneq0b  13983  lsslsp  13985  sraring  14005  sralmod  14006  rspssp  14050  rnglidlmsgrp  14053  2idlcpblrng  14079  gsumfzfsumlem0  14142  zncrng  14201  znzrh2  14202  znzrhfo  14204  znf1o  14207  znfi  14211  znhash  14212  znidom  14213  znidomb  14214  znunit  14215  znrrg  14216  psrbaglesuppg  14226  psrelbas  14228  ntridm  14362  ntrtop  14364  ntrcls0  14367  ntr0  14370  isopn3i  14371  neiss2  14378  opnneiss  14394  topssnei  14398  cnpf2  14443  icnpimaex  14447  lmcvg  14453  iscnp4  14454  cncnp  14466  cnptopresti  14474  lmfss  14480  lmtopcnp  14486  hmeores  14551  bldisj  14637  xblss2ps  14640  xblss2  14641  blhalf  14644  blssps  14663  blss  14664  ssblex  14667  blpnfctr  14675  xmetresbl  14676  mopni2  14719  bdxmet  14737  bdbl  14739  xmetxpbl  14744  metcnpi  14751  metcnpi2  14752  tgioo  14790  rescncf  14817  mulcncflem  14843  cnopnap  14847  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeu  14859  dedekindicclemuub  14862  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemicc  14868  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthdec  14880  ivthreinc  14881  hovergt0  14886  dich0  14888  limcimolemlt  14900  cnplimcim  14903  cnplimclemr  14905  limccnpcntop  14911  limccnp2cntop  14913  limccoap  14914  dvfgg  14924  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvaddxxbr  14937  dvmulxxbr  14938  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  dvcoapbr  14943  dvcjbr  14944  dvcj  14945  dvrecap  14949  dvmptclx  14954  dveflem  14962  elply2  14971  plyf  14973  plyaddlem  14985  plymullem  14986  plycoeid3  14993  plyco  14995  plycj  14997  dvply1  15001  dvply2g  15002  reeff1oleme  15008  eflt  15011  sin0pilem1  15017  pilem3  15019  cosq14gt0  15068  coseq0negpitopi  15072  tangtx  15074  coskpi  15084  cosordlem  15085  cosq34lt1  15086  relogef  15100  logrpap0d  15114  rplogcl  15115  logge0  15116  logdivlti  15117  cxplt3  15156  rpabscxpbnd  15176  dvdsppwf1o  15225  fsumdvdsmul  15227  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgslem1  15241  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsvalmod  15260  lgsfcl3  15262  lgsmod  15267  lgsdirprm  15275  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem3  15304  gausslemma2dlem4  15305  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  lgsquad2lem2  15323  lgsquad3  15325  2lgslem1c  15331  2lgsoddprm  15354  2sqlem3  15358  2sqlem4  15359  2sqlem8  15364  bj-charfunr  15456  pwf1oexmid  15644  subctctexmid  15645  pw1nct  15647  nnsf  15649  peano4nninf  15650  nninfsellemeq  15658  cvgcmp2nlemabs  15676  iooref1o  15678  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  apdifflemf  15690  apdifflemr  15691  apdiff  15692  iswomninnlem  15693  redcwlpo  15699  redc0  15701  reap0  15702  nconstwlpolemgt0  15708  neapmkvlem  15711  ltlenmkv  15714  supfz  15715  inffz  15716