Theorem mpbid 147

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbid.min	⊢ (𝜑 → 𝜓)
mpbid.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbid	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 ⊢ (𝜑 → 𝜓)
2		mpbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

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  2764  vtoclgft  2788  vtoclegft  2810  elrab3t  2893  eueq2dc  2911  sbceq1dd  2969  csbiedf  3098  sseqtrd  3194  3sstr3d  3200  ifbothdadc  3567  snssd  3738  dfnfc2  3828  breqdi  4019  breqtrd  4030  3brtr3d  4035  csbexga  4132  reuhypd  4472  reg2exmidlema  4534  elirr  4541  en2lp  4554  onsucuni2  4564  finds  4600  iota4  5197  iota4an  5198  funimaexglem  5300  fneu  5321  fco2  5383  fssres2  5394  fresin  5395  feu  5399  f1orescnv  5478  resdif  5484  funcocnv2  5487  f1oprg  5506  fvelrnb  5564  fimacnv  5646  f1oresrab  5682  fsn2  5691  xpsng  5692  fnressn  5703  fsnunf  5717  foeqcnvco  5791  isores1  5815  isoini2  5820  riota5f  5855  riotass2  5857  riotass  5858  ovmpodxf  6000  elopabi  6196  cnvf1o  6226  smores3  6294  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  rdgon  6387  frecabcl  6400  frecsuclem  6407  nnsucsssuc  6493  nnsucuniel  6496  erref  6555  iserd  6561  swoer  6563  swoord1  6564  swoord2  6565  erth  6579  erthi  6581  eroveu  6626  pmresg  6676  mapsn  6690  fndmeng  6810  xpen  6845  phplem4  6855  phplem4on  6867  fidifsnen  6870  dif1en  6879  dif1enen  6880  fisbth  6883  diffisn  6893  ac6sfi  6898  fimax2gtri  6901  en2eqpr  6907  unsnfidcex  6919  unsnfidcel  6920  fiintim  6928  fidcenumlemrks  6952  elfi2  6971  elfir  6972  fiuni  6977  fifo  6979  eqsupti  6995  supisoti  7009  ordiso2  7034  casef  7087  difinfsnlem  7098  ctmlemr  7107  ctssdccl  7110  enumct  7114  nnnninfeq  7126  nnnninfeq2  7127  enomnilem  7136  exmidomni  7140  fodjum  7144  fodjuomnilemres  7146  mkvprop  7156  enmkvlem  7159  enwomnilem  7167  nninfdcinf  7169  nninfwlpoimlemdc  7175  acfun  7206  2omotaplemap  7256  exmidmotap  7260  ccfunen  7263  cc2lem  7265  dfplpq2  7353  ltanqi  7401  ltmnqi  7402  ltaddnq  7406  subhalfnqq  7413  ltbtwnnqq  7414  archnqq  7416  prarloclemarch2  7418  enq0sym  7431  enq0ref  7432  enq0tr  7433  nqnq0pi  7437  nnnq0lem1  7445  distrnq0  7458  prarloclemlt  7492  prarloclemn  7498  prarloclemcalc  7501  genplt2i  7509  addnqprllem  7526  addnqprulem  7527  addlocprlemgt  7533  appdivnq  7562  prmuloc2  7566  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemru  7611  prplnqu  7619  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemladdfu  7653  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  archrecnq  7662  archrecpr  7663  caucvgprlemk  7664  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgprprlemk  7682  caucvgprprlemnkeqj  7689  caucvgprprlemnbj  7692  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemexbt  7705  caucvgprprlemexb  7706  caucvgprprlem1  7708  caucvgprprlem2  7709  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  prsrlem1  7741  addgt0sr  7774  srpospr  7782  prsrriota  7787  caucvgsrlemgt1  7794  caucvgsrlemoffgt1  7798  caucvgsr  7801  mappsrprg  7803  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  recriota  7889  axsuploc  8030  lelttr  8046  ltletr  8047  ltnsymd  8077  lensymd  8079  cnegexlem3  8134  cnegex2  8136  addcanad  8143  addcan2ad  8144  negcon1ad  8263  negne0d  8266  negrebd  8267  subeq0d  8276  subne0ad  8279  neg11d  8280  subcand  8309  subcan2d  8310  ltadd2  8376  ltadd2dd  8379  add20  8431  ltnegcon1d  8482  ltnegcon2d  8483  lenegcon1d  8484  lenegcon2d  8485  subled  8505  lesubd  8506  ltsub23d  8507  ltsub13d  8508  ltadd1dd  8513  ltsub1dd  8514  ltsub2dd  8515  leadd1dd  8516  leadd2dd  8517  lesub1dd  8518  lesub2dd  8519  recexre  8535  apreap  8544  ltmul1a  8548  reapmul1  8552  cru  8559  apreim  8560  mulge0  8576  leltap  8582  negap0d  8588  ltleap  8589  ltapd  8595  ap0gt0  8597  ap0gt0d  8598  mulcanapad  8620  mulcanap2ad  8621  eqnegad  8691  diveqap0d  8754  diveqap1d  8755  divap1d  8758  rec11apd  8768  div11apd  8788  div2subap  8794  recgt0  8807  prodgt0  8809  lemul1a  8815  lemulge12  8824  lt2msq1  8842  lediv12a  8851  recreclt  8857  nn1suc  8938  nnnlt1  8945  nn2ge  8952  nn1gt1  8953  nnrecl  9174  nn0nlt0  9202  elnn0z  9266  nn0negleid  9321  elz2  9324  nn0n0n1ge2b  9332  nnm1ge0  9339  nn0ge0div  9340  zextle  9344  suprzclex  9351  nn0ind-raph  9370  zindd  9371  uzneg  9546  eluzadd  9556  eluzsub  9557  uzm1  9558  uz3m2nn  9573  supminfex  9597  infregelbex  9598  nn01to3  9617  ltrec1d  9717  lerec2d  9718  ledivdivd  9722  divge1  9723  ltmul1dd  9752  ltmul2dd  9753  ltdiv1dd  9754  lediv1dd  9755  ltdiv23d  9757  lediv23d  9758  nn0ledivnn  9767  addlelt  9768  xrlelttr  9806  xrltletr  9807  xaddass2  9870  xltadd1  9876  xlt2add  9880  ixxdisj  9903  icoshftf1o  9991  icodisj  9992  lincmb01cmp  10003  iccf1o  10004  uzsubsubfz  10047  fzdisj  10052  fzopth  10061  fznatpl1  10076  fzsuc2  10079  fzp1disj  10080  fzrev2i  10086  uzdisj  10093  fseq1p1m1  10094  fzm1  10100  fzneuz  10101  fzp1nel  10104  fzrevral  10105  fznn0sub2  10128  fz0fzdiffz0  10130  difelfzle  10134  difelfznle  10135  nn0disj  10138  fzonnsub  10169  fzodisj  10178  fzouzdisj  10180  eluzgtdifelfzo  10197  ubmelfzo  10200  fzonn0p1p1  10213  ubmelm1fzo  10226  fzostep1  10237  exfzdc  10240  subfzo0  10242  qtri3or  10243  exbtwnzlemex  10250  rebtwn2z  10255  qbtwnrelemcalc  10256  qbtwnre  10257  qavgle  10259  apbtwnz  10274  flid  10284  flqwordi  10288  flqmulnn0  10299  flhalf  10302  flltdivnn0lt  10304  fldiv4p1lem1div2  10305  intfracq  10320  flqdiv  10321  flqpmodeq  10327  modqmulnn  10342  mulqaddmodid  10364  modqmuladdim  10367  modqmuladdnn0  10368  m1modge3gt1  10371  q2submod  10385  modaddmodup  10387  modqsubdir  10393  modqeqmodmin  10394  modfzo0difsn  10395  uzennn  10436  uzsinds  10442  monoord2  10477  ser3mono  10478  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemqf1o  10493  iseqf1olemqk  10494  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1olemp  10502  ser3le  10518  exp3val  10522  expnegap0  10528  expgt1  10558  ltexp2a  10572  le2sq2  10596  nnlesq  10624  qsqeqor  10631  bernneq  10641  expnbnd  10644  expnlbnd  10645  expnlbnd2  10646  expeq0d  10650  sq11d  10687  nn0ltexp2  10689  expcand  10697  nn0opthd  10702  facdiv  10718  faclbnd6  10724  facubnd  10725  facavg  10726  bcval4  10732  bcp1nk  10742  bcval5  10743  bcpasc  10746  hashennnuni  10759  isfinite4im  10772  hashnncl  10775  hashunlem  10784  fiprsshashgt1  10797  hashfzp1  10804  zfz1isolemiso  10819  seq3coll  10822  seq3shft  10847  cjth  10855  cjdivap  10918  cjne0d  10956  cjap0d  10957  cvg1nlemcxze  10991  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniq  11004  resqrexlemover  11019  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnmsq  11026  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemglsq  11031  resqrexlemga  11032  leabs  11083  absrele  11092  nn0abscl  11094  ltabs  11096  abslt  11097  absle  11098  abstri  11113  amgm2  11127  sqr11d  11182  abs00d  11195  maxabsle  11213  maxabslemlub  11216  maxleastlt  11224  maxltsup  11227  2zsupmax  11234  minmax  11238  2zinfmin  11251  xrmaxleim  11252  xrmaxiflemlub  11256  xrmaxiflemcom  11257  xrmaxiflemval  11258  xrmaxleastlt  11264  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  xrminmax  11273  xrmin1inf  11275  xrmin2inf  11276  xrmineqinf  11277  climi  11295  reccn2ap  11321  climge0  11333  climle  11342  climserle  11353  climrecvg1n  11356  fz1f1o  11383  summodclem3  11388  summodclem2a  11389  summodc  11391  fisumss  11400  fsum0diaglem  11448  mptfzshft  11450  fsumrev  11451  fisum0diag2  11455  fsumlessfi  11468  fsumle  11471  fsumlt  11472  isumsplit  11499  isumrpcl  11502  expcnvap0  11510  geosergap  11514  pwm1geoserap1  11516  absgtap  11518  geolim  11519  geolim2  11520  georeclim  11521  geoisumr  11526  geoisum1c  11528  cvgratnnlembern  11531  cvgratnnlemseq  11534  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratnn  11539  cvgratz  11540  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodmodclem2a  11584  prodmodc  11586  zproddc  11587  fprodntrivap  11592  fprodf1o  11596  fprodssdc  11598  fprodsplitdc  11604  fprodrev  11627  fprodmodd  11649  efcllemp  11666  ege2le3  11679  eftlcvg  11695  eftlub  11698  efltim  11706  eflegeo  11709  tanaddap  11747  sinbnd  11760  cosbnd  11761  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  cos01gt0  11770  cos12dec  11775  eirraplem  11784  zdvdsdc  11819  dvdstr  11835  dvdsadd2b  11847  dvdslelemd  11849  divconjdvds  11855  alzdvds  11860  dvdsext  11861  fzm1ndvds  11862  fzo0dvdseq  11863  zeo3  11873  even2n  11879  mod2eq1n2dvds  11884  nn0ehalf  11908  nnehalf  11909  nno  11911  nn0oddm1d2  11914  divalglemnqt  11925  divalglemex  11927  divalglemeuneg  11928  divalg2  11931  divalgmod  11932  flodddiv4t2lthalf  11942  zsupcllemstep  11946  infssuzex  11950  zsupssdc  11955  dvdsbnd  11957  gcdsupex  11958  gcdsupcl  11959  gcddvds  11964  divgcdz  11972  divgcdnn  11976  gcd0id  11980  gcdneg  11983  gcd1  11988  dvdsgcdidd  11995  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmo  12007  bezoutlemsup  12010  dfgcd3  12011  bezout  12012  dfgcd2  12015  mulgcd  12017  sqgcd  12030  dvdssqlem  12031  bezoutr1  12034  uzwodc  12038  lcmval  12063  lcmcllem  12067  dvdslcm  12069  lcmgcdlem  12077  lcmdvds  12079  lcmgcdeq  12083  ncoprmgcdne1b  12089  mulgcddvds  12094  rpmulgcd2  12095  qredeu  12097  rpdvds  12099  prmind2  12120  nprm  12123  dvdsnprmd  12125  isprm5lem  12141  isprm5  12142  divgcdodd  12143  isprm6  12147  prmexpb  12151  pw2dvds  12166  pw2dvdseulemle  12167  oddpwdclemdc  12173  sqne2sq  12177  znege1  12178  sqrt2irraplemnn  12179  divnumden  12196  divdenle  12197  qden1elz  12205  nn0sqrtelqelz  12206  hashdvds  12221  crth  12224  phimullem  12225  eulerthlemfi  12228  eulerthlemh  12231  eulerthlemth  12232  eulerth  12233  prmdiv  12235  prmdiveq  12236  hashgcdlem  12238  phisum  12240  odzcllem  12242  odzdvds  12245  odzphi  12246  oddprm  12259  pythagtriplem3  12267  pythagtriplem4  12268  pythagtriplem10  12269  pythagtriplem11  12274  pythagtriplem13  12276  pythagtriplem19  12282  pcprendvds  12290  pcprendvds2  12291  pcpre1  12292  pcpremul  12293  pceulem  12294  pceu  12295  pczpre  12297  pcmul  12301  pcdiv  12302  pcqmul  12303  pcqdiv  12307  pcexp  12309  pcidlem  12322  pcneg  12324  pcdvdstr  12326  pcgcd1  12327  pc2dvds  12329  dvdsprmpweq  12334  dvdsprmpweqle  12336  pcaddlem  12338  pcadd  12339  pcmpt  12341  fldivp1  12346  pcfaclem  12347  pcfac  12348  pcbc  12349  qexpz  12350  oddprmdvds  12352  pockthlem  12354  pockthg  12355  infpnlem2  12358  1arith  12365  4sqlem9  12384  4sqlem10  12385  oddennn  12393  ennnfonelemk  12401  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemrnh  12417  ennnfonelemen  12422  ennnfonelemim  12425  ctinfomlemom  12428  ctiunctlemf  12439  ssnnctlemct  12447  nninfdclemcl  12449  nninfdclemp1  12451  nninfdclemlt  12452  unbendc  12455  mgmb1mgm1  12787  mgm1  12789  mgmidsssn0  12803  sgrp1  12816  sgrpidmndm  12821  ismndd  12838  mhmpropd  12857  isgrpd2e  12896  grpidd2  12914  isgrpinv  12926  grpinvinv  12937  grpidssd  12946  grpinvssd  12947  mulgval  12986  mulgfng  12987  mulgnegnn  12993  subg0  13040  issubg4m  13053  nsgconj  13066  1nsgtrivd  13079  eqgen  13086  eqgcpbl  13087  issrgid  13164  srg1zr  13170  ringcl  13196  isringid  13208  ringcom  13214  ringpropd  13217  ringlz  13222  ringrz  13223  ring1  13236  opprring  13249  dvdsrcld  13266  unitcld  13277  unitmulcl  13282  unitgrp  13285  unitnegcl  13299  subrgugrp  13361  aprsym  13374  islmodd  13383  lmod0vs  13411  lmodfopne  13416  lmodcom  13423  ntridm  13629  ntrtop  13631  ntrcls0  13634  ntr0  13637  isopn3i  13638  neiss2  13645  opnneiss  13661  topssnei  13665  cnpf2  13710  icnpimaex  13714  lmcvg  13720  iscnp4  13721  cncnp  13733  cnptopresti  13741  lmfss  13747  lmtopcnp  13753  hmeores  13818  bldisj  13904  xblss2ps  13907  xblss2  13908  blhalf  13911  blssps  13930  blss  13931  ssblex  13934  blpnfctr  13942  xmetresbl  13943  mopni2  13986  bdxmet  14004  bdbl  14006  xmetxpbl  14011  metcnpi  14018  metcnpi2  14019  tgioo  14049  rescncf  14071  mulcncflem  14093  cnopnap  14097  dedekindeulemuub  14098  dedekindeulemloc  14100  dedekindeulemlu  14102  dedekindeu  14104  dedekindicclemuub  14107  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicclemicc  14113  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthdec  14125  limcimolemlt  14136  cnplimcim  14139  cnplimclemr  14141  limccnpcntop  14147  limccnp2cntop  14149  limccoap  14150  dvfgg  14160  dvidlemap  14163  dvaddxxbr  14168  dvmulxxbr  14169  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvcoapbr  14174  dvcjbr  14175  dvcj  14176  dvrecap  14180  dvmptclx  14183  dveflem  14190  reeff1oleme  14196  eflt  14199  sin0pilem1  14205  pilem3  14207  cosq14gt0  14256  coseq0negpitopi  14260  tangtx  14262  coskpi  14272  cosordlem  14273  cosq34lt1  14274  relogef  14288  logrpap0d  14302  rplogcl  14303  logge0  14304  logdivlti  14305  cxplt3  14343  rpabscxpbnd  14362  lgslem1  14404  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsvalmod  14423  lgsfcl3  14425  lgsmod  14430  lgsdirprm  14438  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  2sqlem3  14467  2sqlem4  14468  2sqlem8  14473  bj-charfunr  14565  pwf1oexmid  14752  subctctexmid  14753  pw1nct  14755  nnsf  14757  peano4nninf  14758  nninfsellemeq  14766  cvgcmp2nlemabs  14783  iooref1o  14785  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trirec0  14795  apdifflemf  14797  apdifflemr  14798  apdiff  14799  iswomninnlem  14800  redcwlpo  14806  redc0  14808  reap0  14809  nconstwlpolemgt0  14814  neapmkvlem  14817  ltlenmkv  14820  supfz  14821  inffz  14822