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  5566  fimacnv  5648  f1oresrab  5684  fsn2  5693  xpsng  5694  fnressn  5705  fsnunf  5719  foeqcnvco  5794  isores1  5818  isoini2  5823  riota5f  5858  riotass2  5860  riotass  5861  ovmpodxf  6003  elopabi  6199  cnvf1o  6229  smores3  6297  tfrlemisucaccv  6329  tfr1onlemsucaccv  6345  tfrcllemsucaccv  6358  rdgon  6390  frecabcl  6403  frecsuclem  6410  nnsucsssuc  6496  nnsucuniel  6499  erref  6558  iserd  6564  swoer  6566  swoord1  6567  swoord2  6568  erth  6582  erthi  6584  eroveu  6629  pmresg  6679  mapsn  6693  fndmeng  6813  xpen  6848  phplem4  6858  phplem4on  6870  fidifsnen  6873  dif1en  6882  dif1enen  6883  fisbth  6886  diffisn  6896  ac6sfi  6901  fimax2gtri  6904  en2eqpr  6910  unsnfidcex  6922  unsnfidcel  6923  fiintim  6931  fidcenumlemrks  6955  elfi2  6974  elfir  6975  fiuni  6980  fifo  6982  eqsupti  6998  supisoti  7012  ordiso2  7037  casef  7090  difinfsnlem  7101  ctmlemr  7110  ctssdccl  7113  enumct  7117  nnnninfeq  7129  nnnninfeq2  7130  enomnilem  7139  exmidomni  7143  fodjum  7147  fodjuomnilemres  7149  mkvprop  7159  enmkvlem  7162  enwomnilem  7170  nninfdcinf  7172  nninfwlpoimlemdc  7178  acfun  7209  2omotaplemap  7259  exmidmotap  7263  ccfunen  7266  cc2lem  7268  dfplpq2  7356  ltanqi  7404  ltmnqi  7405  ltaddnq  7409  subhalfnqq  7416  ltbtwnnqq  7417  archnqq  7419  prarloclemarch2  7421  enq0sym  7434  enq0ref  7435  enq0tr  7436  nqnq0pi  7440  nnnq0lem1  7448  distrnq0  7461  prarloclemlt  7495  prarloclemn  7501  prarloclemcalc  7504  genplt2i  7512  addnqprllem  7529  addnqprulem  7530  addlocprlemgt  7536  appdivnq  7565  prmuloc2  7569  ltexprlemopl  7603  ltexprlemopu  7605  ltexprlemru  7614  prplnqu  7622  cauappcvgprlemopl  7648  cauappcvgprlemlol  7649  cauappcvgprlemladdfu  7656  cauappcvgprlemladdrl  7659  cauappcvgprlem1  7661  archrecnq  7665  archrecpr  7666  caucvgprlemk  7667  caucvgprlemnbj  7669  caucvgprlemm  7670  caucvgprlemopl  7671  caucvgprlemlol  7672  caucvgprlemladdfu  7679  caucvgprlemladdrl  7680  caucvgprlem1  7681  caucvgprprlemk  7685  caucvgprprlemnkeqj  7692  caucvgprprlemnbj  7695  caucvgprprlemml  7696  caucvgprprlemmu  7697  caucvgprprlemopl  7699  caucvgprprlemlol  7700  caucvgprprlemopu  7701  caucvgprprlemexbt  7708  caucvgprprlemexb  7709  caucvgprprlem1  7711  caucvgprprlem2  7712  suplocexprlemru  7721  suplocexprlemdisj  7722  suplocexprlemloc  7723  suplocexprlemub  7725  suplocexprlemlub  7726  prsrlem1  7744  addgt0sr  7777  srpospr  7785  prsrriota  7790  caucvgsrlemgt1  7797  caucvgsrlemoffgt1  7801  caucvgsr  7804  mappsrprg  7806  suplocsrlemb  7808  suplocsrlempr  7809  suplocsrlem  7810  recriota  7892  axsuploc  8033  lelttr  8049  ltletr  8050  ltnsymd  8080  lensymd  8082  cnegexlem3  8137  cnegex2  8139  addcanad  8146  addcan2ad  8147  negcon1ad  8266  negne0d  8269  negrebd  8270  subeq0d  8279  subne0ad  8282  neg11d  8283  subcand  8312  subcan2d  8313  ltadd2  8379  ltadd2dd  8382  add20  8434  ltnegcon1d  8485  ltnegcon2d  8486  lenegcon1d  8487  lenegcon2d  8488  subled  8508  lesubd  8509  ltsub23d  8510  ltsub13d  8511  ltadd1dd  8516  ltsub1dd  8517  ltsub2dd  8518  leadd1dd  8519  leadd2dd  8520  lesub1dd  8521  lesub2dd  8522  recexre  8538  apreap  8547  ltmul1a  8551  reapmul1  8555  cru  8562  apreim  8563  mulge0  8579  leltap  8585  negap0d  8591  ltleap  8592  ltapd  8598  ap0gt0  8600  ap0gt0d  8601  mulcanapad  8623  mulcanap2ad  8624  eqnegad  8694  diveqap0d  8757  diveqap1d  8758  divap1d  8761  rec11apd  8771  div11apd  8791  div2subap  8797  recgt0  8810  prodgt0  8812  lemul1a  8818  lemulge12  8827  lt2msq1  8845  lediv12a  8854  recreclt  8860  nn1suc  8941  nnnlt1  8948  nn2ge  8955  nn1gt1  8956  nnrecl  9177  nn0nlt0  9205  elnn0z  9269  nn0negleid  9324  elz2  9327  nn0n0n1ge2b  9335  nnm1ge0  9342  nn0ge0div  9343  zextle  9347  suprzclex  9354  nn0ind-raph  9373  zindd  9374  uzneg  9549  eluzadd  9559  eluzsub  9560  uzm1  9561  uz3m2nn  9576  supminfex  9600  infregelbex  9601  nn01to3  9620  ltrec1d  9720  lerec2d  9721  ledivdivd  9725  divge1  9726  ltmul1dd  9755  ltmul2dd  9756  ltdiv1dd  9757  lediv1dd  9758  ltdiv23d  9760  lediv23d  9761  nn0ledivnn  9770  addlelt  9771  xrlelttr  9809  xrltletr  9810  xaddass2  9873  xltadd1  9879  xlt2add  9883  ixxdisj  9906  icoshftf1o  9994  icodisj  9995  lincmb01cmp  10006  iccf1o  10007  uzsubsubfz  10050  fzdisj  10055  fzopth  10064  fznatpl1  10079  fzsuc2  10082  fzp1disj  10083  fzrev2i  10089  uzdisj  10096  fseq1p1m1  10097  fzm1  10103  fzneuz  10104  fzp1nel  10107  fzrevral  10108  fznn0sub2  10131  fz0fzdiffz0  10133  difelfzle  10137  difelfznle  10138  nn0disj  10141  fzonnsub  10172  fzodisj  10181  fzouzdisj  10183  eluzgtdifelfzo  10200  ubmelfzo  10203  fzonn0p1p1  10216  ubmelm1fzo  10229  fzostep1  10240  exfzdc  10243  subfzo0  10245  qtri3or  10246  exbtwnzlemex  10253  rebtwn2z  10258  qbtwnrelemcalc  10259  qbtwnre  10260  qavgle  10262  apbtwnz  10277  flid  10287  flqwordi  10291  flqmulnn0  10302  flhalf  10305  flltdivnn0lt  10307  fldiv4p1lem1div2  10308  intfracq  10323  flqdiv  10324  flqpmodeq  10330  modqmulnn  10345  mulqaddmodid  10367  modqmuladdim  10370  modqmuladdnn0  10371  m1modge3gt1  10374  q2submod  10388  modaddmodup  10390  modqsubdir  10396  modqeqmodmin  10397  modfzo0difsn  10398  uzennn  10439  uzsinds  10445  monoord2  10480  ser3mono  10481  iseqf1olemqcl  10489  iseqf1olemnab  10491  iseqf1olemab  10492  iseqf1olemqf1o  10496  iseqf1olemqk  10497  seq3f1olemqsumkj  10501  seq3f1olemqsumk  10502  seq3f1olemqsum  10503  seq3f1olemp  10505  ser3le  10521  exp3val  10525  expnegap0  10531  expgt1  10561  ltexp2a  10575  le2sq2  10599  nnlesq  10627  qsqeqor  10634  bernneq  10644  expnbnd  10647  expnlbnd  10648  expnlbnd2  10649  expeq0d  10653  sq11d  10690  nn0ltexp2  10692  expcand  10700  nn0opthd  10705  facdiv  10721  faclbnd6  10727  facubnd  10728  facavg  10729  bcval4  10735  bcp1nk  10745  bcval5  10746  bcpasc  10749  hashennnuni  10762  isfinite4im  10775  hashnncl  10778  hashunlem  10787  fiprsshashgt1  10800  hashfzp1  10807  zfz1isolemiso  10822  seq3coll  10825  seq3shft  10850  cjth  10858  cjdivap  10921  cjne0d  10959  cjap0d  10960  cvg1nlemcxze  10994  cvg1nlemcau  10996  cvg1nlemres  10997  recvguniq  11007  resqrexlemover  11022  resqrexlemdecn  11024  resqrexlemlo  11025  resqrexlemcalc2  11027  resqrexlemcalc3  11028  resqrexlemnmsq  11029  resqrexlemnm  11030  resqrexlemcvg  11031  resqrexlemglsq  11034  resqrexlemga  11035  leabs  11086  absrele  11095  nn0abscl  11097  ltabs  11099  abslt  11100  absle  11101  abstri  11116  amgm2  11130  sqr11d  11185  abs00d  11198  maxabsle  11216  maxabslemlub  11219  maxleastlt  11227  maxltsup  11230  2zsupmax  11237  minmax  11241  2zinfmin  11254  xrmaxleim  11255  xrmaxiflemlub  11259  xrmaxiflemcom  11260  xrmaxiflemval  11261  xrmaxleastlt  11267  xrmaxltsup  11269  xrmaxaddlem  11271  xrmaxadd  11272  xrminmax  11276  xrmin1inf  11278  xrmin2inf  11279  xrmineqinf  11280  climi  11298  reccn2ap  11324  climge0  11336  climle  11345  climserle  11356  climrecvg1n  11359  fz1f1o  11386  summodclem3  11391  summodclem2a  11392  summodc  11394  fisumss  11403  fsum0diaglem  11451  mptfzshft  11453  fsumrev  11454  fisum0diag2  11458  fsumlessfi  11471  fsumle  11474  fsumlt  11475  isumsplit  11502  isumrpcl  11505  expcnvap0  11513  geosergap  11517  pwm1geoserap1  11519  absgtap  11521  geolim  11522  geolim2  11523  georeclim  11524  geoisumr  11529  geoisum1c  11531  cvgratnnlembern  11534  cvgratnnlemseq  11537  cvgratnnlemsumlt  11539  cvgratnnlemfm  11540  cvgratnnlemrate  11541  cvgratnn  11542  cvgratz  11543  mertenslemub  11545  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  prodmodclem2a  11587  prodmodc  11589  zproddc  11590  fprodntrivap  11595  fprodf1o  11599  fprodssdc  11601  fprodsplitdc  11607  fprodrev  11630  fprodmodd  11652  efcllemp  11669  ege2le3  11682  eftlcvg  11698  eftlub  11701  efltim  11709  eflegeo  11712  tanaddap  11750  sinbnd  11763  cosbnd  11764  sin01bnd  11768  cos01bnd  11769  sin01gt0  11772  cos01gt0  11773  cos12dec  11778  eirraplem  11787  zdvdsdc  11822  dvdstr  11838  dvdsadd2b  11850  dvdslelemd  11852  divconjdvds  11858  alzdvds  11863  dvdsext  11864  fzm1ndvds  11865  fzo0dvdseq  11866  zeo3  11876  even2n  11882  mod2eq1n2dvds  11887  nn0ehalf  11911  nnehalf  11912  nno  11914  nn0oddm1d2  11917  divalglemnqt  11928  divalglemex  11930  divalglemeuneg  11931  divalg2  11934  divalgmod  11935  flodddiv4t2lthalf  11945  zsupcllemstep  11949  infssuzex  11953  zsupssdc  11958  dvdsbnd  11960  gcdsupex  11961  gcdsupcl  11962  gcddvds  11967  divgcdz  11975  divgcdnn  11979  gcd0id  11983  gcdneg  11986  gcd1  11991  dvdsgcdidd  11998  bezoutlemnewy  12000  bezoutlemstep  12001  bezoutlemmo  12010  bezoutlemsup  12013  dfgcd3  12014  bezout  12015  dfgcd2  12018  mulgcd  12020  sqgcd  12033  dvdssqlem  12034  bezoutr1  12037  uzwodc  12041  lcmval  12066  lcmcllem  12070  dvdslcm  12072  lcmgcdlem  12080  lcmdvds  12082  lcmgcdeq  12086  ncoprmgcdne1b  12092  mulgcddvds  12097  rpmulgcd2  12098  qredeu  12100  rpdvds  12102  prmind2  12123  nprm  12126  dvdsnprmd  12128  isprm5lem  12144  isprm5  12145  divgcdodd  12146  isprm6  12150  prmexpb  12154  pw2dvds  12169  pw2dvdseulemle  12170  oddpwdclemdc  12176  sqne2sq  12180  znege1  12181  sqrt2irraplemnn  12182  divnumden  12199  divdenle  12200  qden1elz  12208  nn0sqrtelqelz  12209  hashdvds  12224  crth  12227  phimullem  12228  eulerthlemfi  12231  eulerthlemh  12234  eulerthlemth  12235  eulerth  12236  prmdiv  12238  prmdiveq  12239  hashgcdlem  12241  phisum  12243  odzcllem  12245  odzdvds  12248  odzphi  12249  oddprm  12262  pythagtriplem3  12270  pythagtriplem4  12271  pythagtriplem10  12272  pythagtriplem11  12277  pythagtriplem13  12279  pythagtriplem19  12285  pcprendvds  12293  pcprendvds2  12294  pcpre1  12295  pcpremul  12296  pceulem  12297  pceu  12298  pczpre  12300  pcmul  12304  pcdiv  12305  pcqmul  12306  pcqdiv  12310  pcexp  12312  pcidlem  12325  pcneg  12327  pcdvdstr  12329  pcgcd1  12330  pc2dvds  12332  dvdsprmpweq  12337  dvdsprmpweqle  12339  pcaddlem  12341  pcadd  12342  pcmpt  12344  fldivp1  12349  pcfaclem  12350  pcfac  12351  pcbc  12352  qexpz  12353  oddprmdvds  12355  pockthlem  12357  pockthg  12358  infpnlem2  12361  1arith  12368  4sqlem9  12387  4sqlem10  12388  oddennn  12396  ennnfonelemk  12404  ennnfonelemkh  12416  ennnfonelemhf1o  12417  ennnfonelemex  12418  ennnfonelemhom  12419  ennnfonelemrnh  12420  ennnfonelemen  12425  ennnfonelemim  12428  ctinfomlemom  12431  ctiunctlemf  12442  ssnnctlemct  12450  nninfdclemcl  12452  nninfdclemp1  12454  nninfdclemlt  12455  unbendc  12458  mgmb1mgm1  12794  mgm1  12796  mgmidsssn0  12810  sgrp1  12823  sgrpidmndm  12829  ismndd  12846  mhmpropd  12865  isgrpd2e  12904  grpidd2  12922  isgrpinv  12935  grpinvinv  12948  grpidssd  12957  grpinvssd  12958  mulgval  12999  mulgfng  13001  mulgnegnn  13007  subg0  13054  issubg4m  13067  nsgconj  13080  1nsgtrivd  13093  eqgen  13101  eqgcpbl  13102  rnglz  13171  rngrz  13172  issrgid  13202  srg1zr  13208  ringcl  13234  isringid  13246  ringcom  13252  ringpropd  13255  ringlz  13260  ringrz  13261  ring1  13274  opprring  13287  dvdsrcld  13304  unitcld  13315  unitmulcl  13320  unitgrp  13323  unitnegcl  13337  subrgugrp  13399  aprsym  13412  islmodd  13421  lmod0vs  13449  lmodfopne  13454  lmodcom  13461  lssclg  13489  lspsnel5a  13535  lspsneq0b  13552  lsslsp  13554  sraring  13574  sralmod  13575  rspssp  13612  ntridm  13814  ntrtop  13816  ntrcls0  13819  ntr0  13822  isopn3i  13823  neiss2  13830  opnneiss  13846  topssnei  13850  cnpf2  13895  icnpimaex  13899  lmcvg  13905  iscnp4  13906  cncnp  13918  cnptopresti  13926  lmfss  13932  lmtopcnp  13938  hmeores  14003  bldisj  14089  xblss2ps  14092  xblss2  14093  blhalf  14096  blssps  14115  blss  14116  ssblex  14119  blpnfctr  14127  xmetresbl  14128  mopni2  14171  bdxmet  14189  bdbl  14191  xmetxpbl  14196  metcnpi  14203  metcnpi2  14204  tgioo  14234  rescncf  14256  mulcncflem  14278  cnopnap  14282  dedekindeulemuub  14283  dedekindeulemloc  14285  dedekindeulemlu  14287  dedekindeu  14289  dedekindicclemuub  14292  dedekindicclemloc  14294  dedekindicclemlu  14296  dedekindicclemicc  14298  dedekindicc  14299  ivthinclemlopn  14302  ivthinclemuopn  14304  ivthdec  14310  limcimolemlt  14321  cnplimcim  14324  cnplimclemr  14326  limccnpcntop  14332  limccnp2cntop  14334  limccoap  14335  dvfgg  14345  dvidlemap  14348  dvaddxxbr  14353  dvmulxxbr  14354  dvaddxx  14355  dvmulxx  14356  dviaddf  14357  dvimulf  14358  dvcoapbr  14359  dvcjbr  14360  dvcj  14361  dvrecap  14365  dvmptclx  14368  dveflem  14375  reeff1oleme  14381  eflt  14384  sin0pilem1  14390  pilem3  14392  cosq14gt0  14441  coseq0negpitopi  14445  tangtx  14447  coskpi  14457  cosordlem  14458  cosq34lt1  14459  relogef  14473  logrpap0d  14487  rplogcl  14488  logge0  14489  logdivlti  14490  cxplt3  14528  rpabscxpbnd  14547  lgslem1  14589  lgsval  14593  lgsfvalg  14594  lgsval2lem  14599  lgsvalmod  14608  lgsfcl3  14610  lgsmod  14615  lgsdirprm  14623  lgsdir  14624  lgsdilem2  14625  lgsdi  14626  lgsne0  14627  lgseisenlem1  14638  lgseisenlem2  14639  2sqlem3  14652  2sqlem4  14653  2sqlem8  14658  bj-charfunr  14750  pwf1oexmid  14938  subctctexmid  14939  pw1nct  14941  nnsf  14943  peano4nninf  14944  nninfsellemeq  14952  cvgcmp2nlemabs  14969  iooref1o  14971  trilpolemisumle  14975  trilpolemeq1  14977  trilpolemlt1  14978  trirec0  14981  apdifflemf  14983  apdifflemr  14984  apdiff  14985  iswomninnlem  14986  redcwlpo  14992  redc0  14994  reap0  14995  nconstwlpolemgt0  15001  neapmkvlem  15004  ltlenmkv  15007  supfz  15008  inffz  15009