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  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  3222  3sstr3d  3228  ifbothdadc  3594  snssd  3768  dfnfc2  3858  breqdi  4049  breqtrd  4060  3brtr3d  4065  csbexga  4162  reuhypd  4507  reg2exmidlema  4571  elirr  4578  en2lp  4591  onsucuni2  4601  finds  4637  iota4  5239  iota4an  5240  funimaexglem  5342  fneu  5365  fco2  5427  fssres2  5438  fresin  5439  feu  5443  f1orescnv  5523  resdif  5529  funcocnv2  5532  f1oprg  5551  fvelrnb  5611  fimacnv  5694  f1oresrab  5730  fsn2  5739  xpsng  5740  fnressn  5751  fsnunf  5765  foeqcnvco  5840  isores1  5864  isoini2  5869  riota5f  5905  riotass2  5907  riotass  5908  ovmpodxf  6052  uchoice  6204  elopabi  6262  cnvf1o  6292  smores3  6360  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  rdgon  6453  frecabcl  6466  frecsuclem  6473  nnsucsssuc  6559  nnsucuniel  6562  erref  6621  iserd  6627  swoer  6629  swoord1  6630  swoord2  6631  erth  6647  erthi  6649  eroveu  6694  pmresg  6744  mapsn  6758  fndmeng  6878  xpen  6915  phplem4  6925  phplem4on  6937  fidifsnen  6940  dif1en  6949  dif1enen  6950  fisbth  6953  diffisn  6963  ac6sfi  6968  fimax2gtri  6971  en2eqpr  6977  unsnfidcex  6990  unsnfidcel  6991  prfidceq  6998  fiintim  7001  fidcenumlemrks  7028  elfi2  7047  elfir  7048  fiuni  7053  fifo  7055  eqsupti  7071  supisoti  7085  ordiso2  7110  casef  7163  difinfsnlem  7174  ctmlemr  7183  ctssdccl  7186  enumct  7190  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  exmidomni  7217  fodjum  7221  fodjuomnilemres  7223  mkvprop  7233  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlpoimlemdc  7252  acfun  7290  2omotaplemap  7340  exmidmotap  7344  ccfunen  7347  cc2lem  7349  dfplpq2  7438  ltanqi  7486  ltmnqi  7487  ltaddnq  7491  subhalfnqq  7498  ltbtwnnqq  7499  archnqq  7501  prarloclemarch2  7503  enq0sym  7516  enq0ref  7517  enq0tr  7518  nqnq0pi  7522  nnnq0lem1  7530  distrnq0  7543  prarloclemlt  7577  prarloclemn  7583  prarloclemcalc  7586  genplt2i  7594  addnqprllem  7611  addnqprulem  7612  addlocprlemgt  7618  appdivnq  7647  prmuloc2  7651  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemru  7696  prplnqu  7704  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemladdfu  7738  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  archrecnq  7747  archrecpr  7748  caucvgprlemk  7749  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprprlemk  7767  caucvgprprlemnkeqj  7774  caucvgprprlemnbj  7777  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemexbt  7790  caucvgprprlemexb  7791  caucvgprprlem1  7793  caucvgprprlem2  7794  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  prsrlem1  7826  addgt0sr  7859  srpospr  7867  prsrriota  7872  caucvgsrlemgt1  7879  caucvgsrlemoffgt1  7883  caucvgsr  7886  mappsrprg  7888  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  recriota  7974  axsuploc  8116  lelttr  8132  ltletr  8133  ltnsymd  8163  lensymd  8165  cnegexlem3  8220  cnegex2  8222  addcanad  8229  addcan2ad  8230  negcon1ad  8349  negne0d  8352  negrebd  8353  subeq0d  8362  subne0ad  8365  neg11d  8366  subcand  8395  subcan2d  8396  ltadd2  8463  ltadd2dd  8466  add20  8518  ltnegcon1d  8569  ltnegcon2d  8570  lenegcon1d  8571  lenegcon2d  8572  subled  8592  lesubd  8593  ltsub23d  8594  ltsub13d  8595  ltadd1dd  8600  ltsub1dd  8601  ltsub2dd  8602  leadd1dd  8603  leadd2dd  8604  lesub1dd  8605  lesub2dd  8606  recexre  8622  apreap  8631  ltmul1a  8635  reapmul1  8639  cru  8646  apreim  8647  mulge0  8663  leltap  8669  negap0d  8675  ltleap  8676  ltapd  8682  ap0gt0  8684  ap0gt0d  8685  mulcanapad  8707  mulcanap2ad  8708  eqnegad  8778  diveqap0d  8841  diveqap1d  8842  divap1d  8845  rec11apd  8855  div11apd  8875  div2subap  8881  recgt0  8894  prodgt0  8896  lemul1a  8902  lemulge12  8911  lt2msq1  8929  lediv12a  8938  recreclt  8944  nn1suc  9026  nnnlt1  9033  nn2ge  9040  nn1gt1  9041  nnrecl  9264  nn0nlt0  9292  elnn0z  9356  nn0negleid  9411  elz2  9414  nn0n0n1ge2b  9422  nnm1ge0  9429  nn0ge0div  9430  zextle  9434  suprzclex  9441  nn0ind-raph  9460  zindd  9461  uzneg  9637  eluzadd  9647  eluzsub  9648  uzm1  9649  uz3m2nn  9664  supminfex  9688  infregelbex  9689  nn01to3  9708  irrmulap  9739  ltrec1d  9809  lerec2d  9810  ledivdivd  9814  divge1  9815  ltmul1dd  9844  ltmul2dd  9845  ltdiv1dd  9846  lediv1dd  9847  ltdiv23d  9849  lediv23d  9850  nn0ledivnn  9859  addlelt  9860  xrlelttr  9898  xrltletr  9899  xaddass2  9962  xltadd1  9968  xlt2add  9972  ixxdisj  9995  icoshftf1o  10083  icodisj  10084  lincmb01cmp  10095  iccf1o  10096  uzsubsubfz  10139  fzdisj  10144  fzopth  10153  fznatpl1  10168  fzsuc2  10171  fzp1disj  10172  fzrev2i  10178  uzdisj  10185  fseq1p1m1  10186  fzm1  10192  fzneuz  10193  fzp1nel  10196  fzrevral  10197  fznn0sub2  10220  fz0fzdiffz0  10222  difelfzle  10226  difelfznle  10227  nn0disj  10230  fzonnsub  10262  fzodisj  10271  fzouzdisj  10273  eluzgtdifelfzo  10290  ubmelfzo  10293  fzonn0p1p1  10306  ubmelm1fzo  10319  fzostep1  10330  exfzdc  10333  subfzo0  10335  zsupcllemstep  10336  infssuzex  10340  zsupssdc  10345  qtri3or  10347  exbtwnzlemex  10356  rebtwn2z  10361  qbtwnrelemcalc  10362  qbtwnre  10363  qavgle  10365  apbtwnz  10381  flid  10391  flqwordi  10395  flqmulnn0  10406  flhalf  10409  flltdivnn0lt  10411  fldiv4p1lem1div2  10412  intfracq  10429  flqdiv  10430  flqpmodeq  10436  modqmulnn  10451  mulqaddmodid  10473  modqmuladdim  10476  modqmuladdnn0  10477  m1modge3gt1  10480  q2submod  10494  modaddmodup  10496  modqsubdir  10502  modqeqmodmin  10503  modfzo0difsn  10504  uzennn  10545  uzsinds  10553  monoord2  10595  ser3mono  10596  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemqf1o  10615  iseqf1olemqk  10616  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemp  10624  seqf1oglem1  10628  seqf1oglem2  10629  ser3le  10646  exp3val  10650  expnegap0  10656  expgt1  10686  ltexp2a  10700  le2sq2  10724  nnlesq  10752  qsqeqor  10759  bernneq  10769  expnbnd  10772  expnlbnd  10773  expnlbnd2  10774  expeq0d  10778  sq11d  10815  nn0ltexp2  10818  expcand  10826  nn0opthd  10831  facdiv  10847  faclbnd6  10853  facubnd  10854  facavg  10855  bcval4  10861  bcp1nk  10871  bcval5  10872  bcpasc  10875  hashennnuni  10888  isfinite4im  10901  hashnncl  10904  hashunlem  10913  fiprsshashgt1  10926  hashfzp1  10933  zfz1isolemiso  10948  seq3coll  10951  iswrdiz  10959  wrdffz  10973  seq3shft  11020  cjth  11028  cjdivap  11091  cjne0d  11129  cjap0d  11130  cvg1nlemcxze  11164  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniq  11177  resqrexlemover  11192  resqrexlemdecn  11194  resqrexlemlo  11195  resqrexlemcalc2  11197  resqrexlemcalc3  11198  resqrexlemnmsq  11199  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemglsq  11204  resqrexlemga  11205  leabs  11256  absrele  11265  nn0abscl  11267  ltabs  11269  abslt  11270  absle  11271  abstri  11286  amgm2  11300  sqr11d  11355  abs00d  11368  maxabsle  11386  maxabslemlub  11389  maxleastlt  11397  maxltsup  11400  2zsupmax  11408  minmax  11412  2zinfmin  11425  xrmaxleim  11426  xrmaxiflemlub  11430  xrmaxiflemcom  11431  xrmaxiflemval  11432  xrmaxleastlt  11438  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  xrminmax  11447  xrmin1inf  11449  xrmin2inf  11450  xrmineqinf  11451  climi  11469  reccn2ap  11495  climge0  11507  climle  11516  climserle  11527  climrecvg1n  11530  fz1f1o  11557  summodclem3  11562  summodclem2a  11563  summodc  11565  fisumss  11574  fsum0diaglem  11622  mptfzshft  11624  fsumrev  11625  fisum0diag2  11629  fsumlessfi  11642  fsumle  11645  fsumlt  11646  isumsplit  11673  isumrpcl  11676  expcnvap0  11684  geosergap  11688  pwm1geoserap1  11690  absgtap  11692  geolim  11693  geolim2  11694  georeclim  11695  geoisumr  11700  geoisum1c  11702  cvgratnnlembern  11705  cvgratnnlemseq  11708  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  cvgratz  11714  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodmodclem2a  11758  prodmodc  11760  zproddc  11761  fprodntrivap  11766  fprodf1o  11770  fprodssdc  11772  fprodsplitdc  11778  fprodrev  11801  fprodmodd  11823  efcllemp  11840  ege2le3  11853  eftlcvg  11869  eftlub  11872  efltim  11880  eflegeo  11883  tanaddap  11921  sinbnd  11934  cosbnd  11935  sin01bnd  11939  cos01bnd  11940  sinltxirr  11943  sin01gt0  11944  cos01gt0  11945  cos12dec  11950  eirraplem  11959  zdvdsdc  11994  dvdstr  12010  dvdsadd2b  12022  fsumdvds  12024  dvdslelemd  12025  divconjdvds  12031  alzdvds  12036  dvdsext  12037  fzm1ndvds  12038  fzo0dvdseq  12039  3dvds  12046  zeo3  12050  even2n  12056  mod2eq1n2dvds  12061  nn0ehalf  12085  nnehalf  12086  nno  12088  nn0oddm1d2  12091  divalglemnqt  12102  divalglemex  12104  divalglemeuneg  12105  divalg2  12108  divalgmod  12109  flodddiv4t2lthalf  12121  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitsfi  12139  bitscmp  12140  bitsinv1lem  12143  bitsinv1  12144  dvdsbnd  12148  gcdsupex  12149  gcdsupcl  12150  gcddvds  12155  divgcdz  12163  divgcdnn  12167  gcd0id  12171  gcdneg  12174  gcd1  12179  dvdsgcdidd  12186  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmo  12198  bezoutlemsup  12201  dfgcd3  12202  bezout  12203  dfgcd2  12206  mulgcd  12208  sqgcd  12221  dvdssqlem  12222  bezoutr1  12225  uzwodc  12229  nninfctlemfo  12232  lcmval  12256  lcmcllem  12260  dvdslcm  12262  lcmgcdlem  12270  lcmdvds  12272  lcmgcdeq  12276  ncoprmgcdne1b  12282  mulgcddvds  12287  rpmulgcd2  12288  qredeu  12290  rpdvds  12292  prmind2  12313  nprm  12316  dvdsnprmd  12318  isprm5lem  12334  isprm5  12335  divgcdodd  12336  isprm6  12340  prmexpb  12344  pw2dvds  12359  pw2dvdseulemle  12360  oddpwdclemdc  12366  sqne2sq  12370  znege1  12371  sqrt2irraplemnn  12372  divnumden  12389  divdenle  12390  qden1elz  12398  nn0sqrtelqelz  12399  hashdvds  12414  crth  12417  phimullem  12418  eulerthlemfi  12421  eulerthlemh  12424  eulerthlemth  12425  eulerth  12426  prmdiv  12428  prmdiveq  12429  hashgcdlem  12431  dvdsfi  12432  phisum  12434  odzcllem  12436  odzdvds  12439  odzphi  12440  oddprm  12453  pythagtriplem3  12461  pythagtriplem4  12462  pythagtriplem10  12463  pythagtriplem11  12468  pythagtriplem13  12470  pythagtriplem19  12476  pcprendvds  12484  pcprendvds2  12485  pcpre1  12486  pcpremul  12487  pceulem  12488  pceu  12489  pczpre  12491  pcmul  12495  pcdiv  12496  pcqmul  12497  pcqdiv  12501  pcexp  12503  pcidlem  12517  pcneg  12519  pcdvdstr  12521  pcgcd1  12522  pc2dvds  12524  dvdsprmpweq  12529  dvdsprmpweqle  12531  pcaddlem  12533  pcadd  12534  pcadd2  12535  pcmpt  12537  fldivp1  12542  pcfaclem  12543  pcfac  12544  pcbc  12545  qexpz  12546  oddprmdvds  12548  pockthlem  12550  pockthg  12551  infpnlem2  12554  1arith  12561  4sqlem9  12580  4sqlem10  12581  4sqlem11  12595  4sqlem12  12596  4sqlem13m  12597  4sqlem14  12598  4sqlem16  12600  oddennn  12634  ennnfonelemk  12642  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemrnh  12658  ennnfonelemen  12663  ennnfonelemim  12666  ctinfomlemom  12669  ctiunctlemf  12680  ssnnctlemct  12688  nninfdclemcl  12690  nninfdclemp1  12692  nninfdclemlt  12693  unbendc  12696  prdsbascl  12991  pwselbas  12996  mgmb1mgm1  13070  mgm1  13072  mgmidsssn0  13086  gsumfzval  13093  gsumress  13097  gsum0g  13098  gsumval2  13099  sgrp1  13113  sgrpidmndm  13122  ismndd  13139  prds0g  13151  mhmpropd  13168  resmhm  13189  resmhm2b  13191  gsumwsubmcl  13198  gsumwmhm  13200  isgrpd2e  13222  grpidd2  13243  isgrpinv  13256  grpinvinv  13269  grpidssd  13278  grpinvssd  13279  mulgval  13328  mulgfng  13330  mulgnegnn  13338  subg0  13386  issubg4m  13399  nsgconj  13412  1nsgtrivd  13425  eqgen  13433  eqgcpbl  13434  qus0  13441  ghmid  13455  resghm  13466  ghmnsgpreima  13475  kerf1ghm  13480  conjsubgen  13484  conjnmz  13485  imasabl  13542  rnglz  13577  rngrz  13578  qusrng  13590  issrgid  13613  srg1zr  13619  ringcl  13645  isringid  13657  ringcom  13663  ringpropd  13670  ringlz  13675  ringrz  13676  ring1  13691  opprrng  13709  opprring  13711  dvdsrcld  13729  unitcld  13740  unitmulcl  13745  unitgrp  13748  unitnegcl  13762  rhmmul  13796  isrhm2d  13797  rhmdvdsr  13807  rhmopp  13808  elrhmunit  13809  rhmunitinv  13810  subrgugrp  13872  aprsym  13916  islmodd  13925  lmod0vs  13953  lmodfopne  13958  lmodcom  13965  lssclg  13996  lspsnel5a  14042  lspsneq0b  14059  lsslsp  14061  sraring  14081  sralmod  14082  rspssp  14126  rnglidlmsgrp  14129  2idlcpblrng  14155  gsumfzfsumlem0  14218  zncrng  14277  znzrh2  14278  znzrhfo  14280  znf1o  14283  znfi  14287  znhash  14288  znidom  14289  znidomb  14290  znunit  14291  znrrg  14292  psrbaglesuppg  14302  psrelbas  14304  psrgrp  14313  psr0  14314  psr1clfi  14316  ntridm  14446  ntrtop  14448  ntrcls0  14451  ntr0  14454  isopn3i  14455  neiss2  14462  opnneiss  14478  topssnei  14482  cnpf2  14527  icnpimaex  14531  lmcvg  14537  iscnp4  14538  cncnp  14550  cnptopresti  14558  lmfss  14564  lmtopcnp  14570  hmeores  14635  bldisj  14721  xblss2ps  14724  xblss2  14725  blhalf  14728  blssps  14747  blss  14748  ssblex  14751  blpnfctr  14759  xmetresbl  14760  mopni2  14803  bdxmet  14821  bdbl  14823  xmetxpbl  14828  metcnpi  14835  metcnpi2  14836  tgioo  14874  rescncf  14901  mulcncflem  14927  cnopnap  14931  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeu  14943  dedekindicclemuub  14946  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemicc  14952  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthdec  14964  ivthreinc  14965  hovergt0  14970  dich0  14972  limcimolemlt  14984  cnplimcim  14987  cnplimclemr  14989  limccnpcntop  14995  limccnp2cntop  14997  limccoap  14998  dvfgg  15008  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvaddxxbr  15021  dvmulxxbr  15022  dvaddxx  15023  dvmulxx  15024  dviaddf  15025  dvimulf  15026  dvcoapbr  15027  dvcjbr  15028  dvcj  15029  dvrecap  15033  dvmptclx  15038  dveflem  15046  elply2  15055  plyf  15057  plyaddlem  15069  plymullem  15070  plycoeid3  15077  plyco  15079  plycj  15081  dvply1  15085  dvply2g  15086  reeff1oleme  15092  eflt  15095  sin0pilem1  15101  pilem3  15103  cosq14gt0  15152  coseq0negpitopi  15156  tangtx  15158  coskpi  15168  cosordlem  15169  cosq34lt1  15170  relogef  15184  logrpap0d  15198  rplogcl  15199  logge0  15200  logdivlti  15201  cxplt3  15240  rpabscxpbnd  15260  dvdsppwf1o  15309  fsumdvdsmul  15311  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgslem1  15325  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsvalmod  15344  lgsfcl3  15346  lgsmod  15351  lgsdirprm  15359  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem3  15388  gausslemma2dlem4  15389  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  lgsquad2lem2  15407  lgsquad3  15409  2lgslem1c  15415  2lgsoddprm  15438  2sqlem3  15442  2sqlem4  15443  2sqlem8  15448  bj-charfunr  15540  2omap  15726  pwf1oexmid  15730  subctctexmid  15731  domomsubct  15732  pw1nct  15734  nnsf  15736  peano4nninf  15737  nninfsellemeq  15745  cvgcmp2nlemabs  15763  iooref1o  15765  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trirec0  15775  apdifflemf  15777  apdifflemr  15778  apdiff  15779  iswomninnlem  15780  redcwlpo  15786  redc0  15788  reap0  15789  nconstwlpolemgt0  15795  neapmkvlem  15798  ltlenmkv  15801  supfz  15802  inffz  15803