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  nninfinfwlpolem  7253  acfun  7292  2omotaplemap  7342  exmidmotap  7346  ccfunen  7349  cc2lem  7351  dfplpq2  7440  ltanqi  7488  ltmnqi  7489  ltaddnq  7493  subhalfnqq  7500  ltbtwnnqq  7501  archnqq  7503  prarloclemarch2  7505  enq0sym  7518  enq0ref  7519  enq0tr  7520  nqnq0pi  7524  nnnq0lem1  7532  distrnq0  7545  prarloclemlt  7579  prarloclemn  7585  prarloclemcalc  7588  genplt2i  7596  addnqprllem  7613  addnqprulem  7614  addlocprlemgt  7620  appdivnq  7649  prmuloc2  7653  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemru  7698  prplnqu  7706  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemladdfu  7740  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  archrecnq  7749  archrecpr  7750  caucvgprlemk  7751  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprprlemk  7769  caucvgprprlemnkeqj  7776  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemexbt  7792  caucvgprprlemexb  7793  caucvgprprlem1  7795  caucvgprprlem2  7796  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  prsrlem1  7828  addgt0sr  7861  srpospr  7869  prsrriota  7874  caucvgsrlemgt1  7881  caucvgsrlemoffgt1  7885  caucvgsr  7888  mappsrprg  7890  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  recriota  7976  axsuploc  8118  lelttr  8134  ltletr  8135  ltnsymd  8165  lensymd  8167  cnegexlem3  8222  cnegex2  8224  addcanad  8231  addcan2ad  8232  negcon1ad  8351  negne0d  8354  negrebd  8355  subeq0d  8364  subne0ad  8367  neg11d  8368  subcand  8397  subcan2d  8398  ltadd2  8465  ltadd2dd  8468  add20  8520  ltnegcon1d  8571  ltnegcon2d  8572  lenegcon1d  8573  lenegcon2d  8574  subled  8594  lesubd  8595  ltsub23d  8596  ltsub13d  8597  ltadd1dd  8602  ltsub1dd  8603  ltsub2dd  8604  leadd1dd  8605  leadd2dd  8606  lesub1dd  8607  lesub2dd  8608  recexre  8624  apreap  8633  ltmul1a  8637  reapmul1  8641  cru  8648  apreim  8649  mulge0  8665  leltap  8671  negap0d  8677  ltleap  8678  ltapd  8684  ap0gt0  8686  ap0gt0d  8687  mulcanapad  8709  mulcanap2ad  8710  eqnegad  8780  diveqap0d  8843  diveqap1d  8844  divap1d  8847  rec11apd  8857  div11apd  8877  div2subap  8883  recgt0  8896  prodgt0  8898  lemul1a  8904  lemulge12  8913  lt2msq1  8931  lediv12a  8940  recreclt  8946  nn1suc  9028  nnnlt1  9035  nn2ge  9042  nn1gt1  9043  nnrecl  9266  nn0nlt0  9294  elnn0z  9358  nn0negleid  9413  elz2  9416  nn0n0n1ge2b  9424  nnm1ge0  9431  nn0ge0div  9432  zextle  9436  suprzclex  9443  nn0ind-raph  9462  zindd  9463  uzneg  9639  eluzadd  9649  eluzsub  9650  uzm1  9651  uz3m2nn  9666  supminfex  9690  infregelbex  9691  nn01to3  9710  irrmulap  9741  ltrec1d  9811  lerec2d  9812  ledivdivd  9816  divge1  9817  ltmul1dd  9846  ltmul2dd  9847  ltdiv1dd  9848  lediv1dd  9849  ltdiv23d  9851  lediv23d  9852  nn0ledivnn  9861  addlelt  9862  xrlelttr  9900  xrltletr  9901  xaddass2  9964  xltadd1  9970  xlt2add  9974  ixxdisj  9997  icoshftf1o  10085  icodisj  10086  lincmb01cmp  10097  iccf1o  10098  uzsubsubfz  10141  fzdisj  10146  fzopth  10155  fznatpl1  10170  fzsuc2  10173  fzp1disj  10174  fzrev2i  10180  uzdisj  10187  fseq1p1m1  10188  fzm1  10194  fzneuz  10195  fzp1nel  10198  fzrevral  10199  fznn0sub2  10222  fz0fzdiffz0  10224  difelfzle  10228  difelfznle  10229  nn0disj  10232  fzonnsub  10264  fzodisj  10273  fzouzdisj  10275  eluzgtdifelfzo  10292  ubmelfzo  10295  fzonn0p1p1  10308  ubmelm1fzo  10321  fzostep1  10332  exfzdc  10335  subfzo0  10337  zsupcllemstep  10338  infssuzex  10342  zsupssdc  10347  qtri3or  10349  exbtwnzlemex  10358  rebtwn2z  10363  qbtwnrelemcalc  10364  qbtwnre  10365  qavgle  10367  apbtwnz  10383  flid  10393  flqwordi  10397  flqmulnn0  10408  flhalf  10411  flltdivnn0lt  10413  fldiv4p1lem1div2  10414  intfracq  10431  flqdiv  10432  flqpmodeq  10438  modqmulnn  10453  mulqaddmodid  10475  modqmuladdim  10478  modqmuladdnn0  10479  m1modge3gt1  10482  q2submod  10496  modaddmodup  10498  modqsubdir  10504  modqeqmodmin  10505  modfzo0difsn  10506  uzennn  10547  uzsinds  10555  monoord2  10597  ser3mono  10598  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemqf1o  10617  iseqf1olemqk  10618  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemp  10626  seqf1oglem1  10630  seqf1oglem2  10631  ser3le  10648  exp3val  10652  expnegap0  10658  expgt1  10688  ltexp2a  10702  le2sq2  10726  nnlesq  10754  qsqeqor  10761  bernneq  10771  expnbnd  10774  expnlbnd  10775  expnlbnd2  10776  expeq0d  10780  sq11d  10817  nn0ltexp2  10820  expcand  10828  nn0opthd  10833  facdiv  10849  faclbnd6  10855  facubnd  10856  facavg  10857  bcval4  10863  bcp1nk  10873  bcval5  10874  bcpasc  10877  hashennnuni  10890  isfinite4im  10903  hashnncl  10906  hashunlem  10915  fiprsshashgt1  10928  hashfzp1  10935  zfz1isolemiso  10950  seq3coll  10953  iswrdiz  10961  wrdffz  10975  seq3shft  11022  cjth  11030  cjdivap  11093  cjne0d  11131  cjap0d  11132  cvg1nlemcxze  11166  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniq  11179  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc2  11199  resqrexlemcalc3  11200  resqrexlemnmsq  11201  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemglsq  11206  resqrexlemga  11207  leabs  11258  absrele  11267  nn0abscl  11269  ltabs  11271  abslt  11272  absle  11273  abstri  11288  amgm2  11302  sqr11d  11357  abs00d  11370  maxabsle  11388  maxabslemlub  11391  maxleastlt  11399  maxltsup  11402  2zsupmax  11410  minmax  11414  2zinfmin  11427  xrmaxleim  11428  xrmaxiflemlub  11432  xrmaxiflemcom  11433  xrmaxiflemval  11434  xrmaxleastlt  11440  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  xrminmax  11449  xrmin1inf  11451  xrmin2inf  11452  xrmineqinf  11453  climi  11471  reccn2ap  11497  climge0  11509  climle  11518  climserle  11529  climrecvg1n  11532  fz1f1o  11559  summodclem3  11564  summodclem2a  11565  summodc  11567  fisumss  11576  fsum0diaglem  11624  mptfzshft  11626  fsumrev  11627  fisum0diag2  11631  fsumlessfi  11644  fsumle  11647  fsumlt  11648  isumsplit  11675  isumrpcl  11678  expcnvap0  11686  geosergap  11690  pwm1geoserap1  11692  absgtap  11694  geolim  11695  geolim2  11696  georeclim  11697  geoisumr  11702  geoisum1c  11704  cvgratnnlembern  11707  cvgratnnlemseq  11710  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  cvgratz  11716  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodmodclem2a  11760  prodmodc  11762  zproddc  11763  fprodntrivap  11768  fprodf1o  11772  fprodssdc  11774  fprodsplitdc  11780  fprodrev  11803  fprodmodd  11825  efcllemp  11842  ege2le3  11855  eftlcvg  11871  eftlub  11874  efltim  11882  eflegeo  11885  tanaddap  11923  sinbnd  11936  cosbnd  11937  sin01bnd  11941  cos01bnd  11942  sinltxirr  11945  sin01gt0  11946  cos01gt0  11947  cos12dec  11952  eirraplem  11961  zdvdsdc  11996  dvdstr  12012  dvdsadd2b  12024  fsumdvds  12026  dvdslelemd  12027  divconjdvds  12033  alzdvds  12038  dvdsext  12039  fzm1ndvds  12040  fzo0dvdseq  12041  3dvds  12048  zeo3  12052  even2n  12058  mod2eq1n2dvds  12063  nn0ehalf  12087  nnehalf  12088  nno  12090  nn0oddm1d2  12093  divalglemnqt  12104  divalglemex  12106  divalglemeuneg  12107  divalg2  12110  divalgmod  12111  flodddiv4t2lthalf  12123  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitsfi  12141  bitscmp  12142  bitsinv1lem  12145  bitsinv1  12146  dvdsbnd  12150  gcdsupex  12151  gcdsupcl  12152  gcddvds  12157  divgcdz  12165  divgcdnn  12169  gcd0id  12173  gcdneg  12176  gcd1  12181  dvdsgcdidd  12188  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmo  12200  bezoutlemsup  12203  dfgcd3  12204  bezout  12205  dfgcd2  12208  mulgcd  12210  sqgcd  12223  dvdssqlem  12224  bezoutr1  12227  uzwodc  12231  nninfctlemfo  12234  lcmval  12258  lcmcllem  12262  dvdslcm  12264  lcmgcdlem  12272  lcmdvds  12274  lcmgcdeq  12278  ncoprmgcdne1b  12284  mulgcddvds  12289  rpmulgcd2  12290  qredeu  12292  rpdvds  12294  prmind2  12315  nprm  12318  dvdsnprmd  12320  isprm5lem  12336  isprm5  12337  divgcdodd  12338  isprm6  12342  prmexpb  12346  pw2dvds  12361  pw2dvdseulemle  12362  oddpwdclemdc  12368  sqne2sq  12372  znege1  12373  sqrt2irraplemnn  12374  divnumden  12391  divdenle  12392  qden1elz  12400  nn0sqrtelqelz  12401  hashdvds  12416  crth  12419  phimullem  12420  eulerthlemfi  12423  eulerthlemh  12426  eulerthlemth  12427  eulerth  12428  prmdiv  12430  prmdiveq  12431  hashgcdlem  12433  dvdsfi  12434  phisum  12436  odzcllem  12438  odzdvds  12441  odzphi  12442  oddprm  12455  pythagtriplem3  12463  pythagtriplem4  12464  pythagtriplem10  12465  pythagtriplem11  12470  pythagtriplem13  12472  pythagtriplem19  12478  pcprendvds  12486  pcprendvds2  12487  pcpre1  12488  pcpremul  12489  pceulem  12490  pceu  12491  pczpre  12493  pcmul  12497  pcdiv  12498  pcqmul  12499  pcqdiv  12503  pcexp  12505  pcidlem  12519  pcneg  12521  pcdvdstr  12523  pcgcd1  12524  pc2dvds  12526  dvdsprmpweq  12531  dvdsprmpweqle  12533  pcaddlem  12535  pcadd  12536  pcadd2  12537  pcmpt  12539  fldivp1  12544  pcfaclem  12545  pcfac  12546  pcbc  12547  qexpz  12548  oddprmdvds  12550  pockthlem  12552  pockthg  12553  infpnlem2  12556  1arith  12563  4sqlem9  12582  4sqlem10  12583  4sqlem11  12597  4sqlem12  12598  4sqlem13m  12599  4sqlem14  12600  4sqlem16  12602  oddennn  12636  ennnfonelemk  12644  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemrnh  12660  ennnfonelemen  12665  ennnfonelemim  12668  ctinfomlemom  12671  ctiunctlemf  12682  ssnnctlemct  12690  nninfdclemcl  12692  nninfdclemp1  12694  nninfdclemlt  12695  unbendc  12698  prdsbascl  12993  pwselbas  12998  mgmb1mgm1  13072  mgm1  13074  mgmidsssn0  13088  gsumfzval  13095  gsumress  13099  gsum0g  13100  gsumval2  13101  sgrp1  13115  sgrpidmndm  13124  ismndd  13141  prds0g  13153  mhmpropd  13170  resmhm  13191  resmhm2b  13193  gsumwsubmcl  13200  gsumwmhm  13202  isgrpd2e  13224  grpidd2  13245  isgrpinv  13258  grpinvinv  13271  grpidssd  13280  grpinvssd  13281  mulgval  13330  mulgfng  13332  mulgnegnn  13340  subg0  13388  issubg4m  13401  nsgconj  13414  1nsgtrivd  13427  eqgen  13435  eqgcpbl  13436  qus0  13443  ghmid  13457  resghm  13468  ghmnsgpreima  13477  kerf1ghm  13482  conjsubgen  13486  conjnmz  13487  imasabl  13544  rnglz  13579  rngrz  13580  qusrng  13592  issrgid  13615  srg1zr  13621  ringcl  13647  isringid  13659  ringcom  13665  ringpropd  13672  ringlz  13677  ringrz  13678  ring1  13693  opprrng  13711  opprring  13713  dvdsrcld  13731  unitcld  13742  unitmulcl  13747  unitgrp  13750  unitnegcl  13764  rhmmul  13798  isrhm2d  13799  rhmdvdsr  13809  rhmopp  13810  elrhmunit  13811  rhmunitinv  13812  subrgugrp  13874  aprsym  13918  islmodd  13927  lmod0vs  13955  lmodfopne  13960  lmodcom  13967  lssclg  13998  lspsnel5a  14044  lspsneq0b  14061  lsslsp  14063  sraring  14083  sralmod  14084  rspssp  14128  rnglidlmsgrp  14131  2idlcpblrng  14157  gsumfzfsumlem0  14220  zncrng  14279  znzrh2  14280  znzrhfo  14282  znf1o  14285  znfi  14289  znhash  14290  znidom  14291  znidomb  14292  znunit  14293  znrrg  14294  psrbaglesuppg  14306  psrelbas  14309  psrelbasfi  14310  psrgrp  14319  psr0  14320  psr1clfi  14322  mplsubgfilemcl  14333  mplsubgfileminv  14334  ntridm  14470  ntrtop  14472  ntrcls0  14475  ntr0  14478  isopn3i  14479  neiss2  14486  opnneiss  14502  topssnei  14506  cnpf2  14551  icnpimaex  14555  lmcvg  14561  iscnp4  14562  cncnp  14574  cnptopresti  14582  lmfss  14588  lmtopcnp  14594  hmeores  14659  bldisj  14745  xblss2ps  14748  xblss2  14749  blhalf  14752  blssps  14771  blss  14772  ssblex  14775  blpnfctr  14783  xmetresbl  14784  mopni2  14827  bdxmet  14845  bdbl  14847  xmetxpbl  14852  metcnpi  14859  metcnpi2  14860  tgioo  14898  rescncf  14925  mulcncflem  14951  cnopnap  14955  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindeulemlu  14965  dedekindeu  14967  dedekindicclemuub  14970  dedekindicclemloc  14972  dedekindicclemlu  14974  dedekindicclemicc  14976  dedekindicc  14977  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthdec  14988  ivthreinc  14989  hovergt0  14994  dich0  14996  limcimolemlt  15008  cnplimcim  15011  cnplimclemr  15013  limccnpcntop  15019  limccnp2cntop  15021  limccoap  15022  dvfgg  15032  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvaddxxbr  15045  dvmulxxbr  15046  dvaddxx  15047  dvmulxx  15048  dviaddf  15049  dvimulf  15050  dvcoapbr  15051  dvcjbr  15052  dvcj  15053  dvrecap  15057  dvmptclx  15062  dveflem  15070  elply2  15079  plyf  15081  plyaddlem  15093  plymullem  15094  plycoeid3  15101  plyco  15103  plycj  15105  dvply1  15109  dvply2g  15110  reeff1oleme  15116  eflt  15119  sin0pilem1  15125  pilem3  15127  cosq14gt0  15176  coseq0negpitopi  15180  tangtx  15182  coskpi  15192  cosordlem  15193  cosq34lt1  15194  relogef  15208  logrpap0d  15222  rplogcl  15223  logge0  15224  logdivlti  15225  cxplt3  15264  rpabscxpbnd  15284  dvdsppwf1o  15333  fsumdvdsmul  15335  mersenne  15341  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgslem1  15349  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsvalmod  15368  lgsfcl3  15370  lgsmod  15375  lgsdirprm  15383  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem3  15412  gausslemma2dlem4  15413  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  lgsquad2lem2  15431  lgsquad3  15433  2lgslem1c  15439  2lgsoddprm  15462  2sqlem3  15466  2sqlem4  15467  2sqlem8  15472  bj-charfunr  15564  2omap  15750  pwf1oexmid  15754  subctctexmid  15755  domomsubct  15756  pw1nct  15758  nnsf  15760  peano4nninf  15761  nninfsellemeq  15769  nnnninfex  15777  cvgcmp2nlemabs  15789  iooref1o  15791  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  trirec0  15801  apdifflemf  15803  apdifflemr  15804  apdiff  15805  iswomninnlem  15806  redcwlpo  15812  redc0  15814  reap0  15815  nconstwlpolemgt0  15821  neapmkvlem  15824  ltlenmkv  15827  supfz  15828  inffz  15829