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  2763  vtoclgft  2787  vtoclegft  2809  elrab3t  2892  eueq2dc  2910  sbceq1dd  2968  csbiedf  3097  sseqtrd  3193  3sstr3d  3199  ifbothdadc  3566  snssd  3737  dfnfc2  3827  breqdi  4018  breqtrd  4029  3brtr3d  4034  csbexga  4131  reuhypd  4471  reg2exmidlema  4533  elirr  4540  en2lp  4553  onsucuni2  4563  finds  4599  iota4  5196  iota4an  5197  funimaexglem  5299  fneu  5320  fco2  5382  fssres2  5393  fresin  5394  feu  5398  f1orescnv  5477  resdif  5483  funcocnv2  5486  f1oprg  5505  fvelrnb  5563  fimacnv  5645  f1oresrab  5681  fsn2  5690  xpsng  5691  fnressn  5702  fsnunf  5716  foeqcnvco  5790  isores1  5814  isoini2  5819  riota5f  5854  riotass2  5856  riotass  5857  ovmpodxf  5999  elopabi  6195  cnvf1o  6225  smores3  6293  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  rdgon  6386  frecabcl  6399  frecsuclem  6406  nnsucsssuc  6492  nnsucuniel  6495  erref  6554  iserd  6560  swoer  6562  swoord1  6563  swoord2  6564  erth  6578  erthi  6580  eroveu  6625  pmresg  6675  mapsn  6689  fndmeng  6809  xpen  6844  phplem4  6854  phplem4on  6866  fidifsnen  6869  dif1en  6878  dif1enen  6879  fisbth  6882  diffisn  6892  ac6sfi  6897  fimax2gtri  6900  en2eqpr  6906  unsnfidcex  6918  unsnfidcel  6919  fiintim  6927  fidcenumlemrks  6951  elfi2  6970  elfir  6971  fiuni  6976  fifo  6978  eqsupti  6994  supisoti  7008  ordiso2  7033  casef  7086  difinfsnlem  7097  ctmlemr  7106  ctssdccl  7109  enumct  7113  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  exmidomni  7139  fodjum  7143  fodjuomnilemres  7145  mkvprop  7155  enmkvlem  7158  enwomnilem  7166  nninfdcinf  7168  nninfwlpoimlemdc  7174  acfun  7205  2omotaplemap  7255  exmidmotap  7259  ccfunen  7262  cc2lem  7264  dfplpq2  7352  ltanqi  7400  ltmnqi  7401  ltaddnq  7405  subhalfnqq  7412  ltbtwnnqq  7413  archnqq  7415  prarloclemarch2  7417  enq0sym  7430  enq0ref  7431  enq0tr  7432  nqnq0pi  7436  nnnq0lem1  7444  distrnq0  7457  prarloclemlt  7491  prarloclemn  7497  prarloclemcalc  7500  genplt2i  7508  addnqprllem  7525  addnqprulem  7526  addlocprlemgt  7532  appdivnq  7561  prmuloc2  7565  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemru  7610  prplnqu  7618  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemladdfu  7652  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  archrecnq  7661  archrecpr  7662  caucvgprlemk  7663  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprprlemk  7681  caucvgprprlemnkeqj  7688  caucvgprprlemnbj  7691  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemexbt  7704  caucvgprprlemexb  7705  caucvgprprlem1  7707  caucvgprprlem2  7708  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  suplocexprlemlub  7722  prsrlem1  7740  addgt0sr  7773  srpospr  7781  prsrriota  7786  caucvgsrlemgt1  7793  caucvgsrlemoffgt1  7797  caucvgsr  7800  mappsrprg  7802  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  recriota  7888  axsuploc  8029  lelttr  8045  ltletr  8046  ltnsymd  8076  lensymd  8078  cnegexlem3  8133  cnegex2  8135  addcanad  8142  addcan2ad  8143  negcon1ad  8262  negne0d  8265  negrebd  8266  subeq0d  8275  subne0ad  8278  neg11d  8279  subcand  8308  subcan2d  8309  ltadd2  8375  ltadd2dd  8378  add20  8430  ltnegcon1d  8481  ltnegcon2d  8482  lenegcon1d  8483  lenegcon2d  8484  subled  8504  lesubd  8505  ltsub23d  8506  ltsub13d  8507  ltadd1dd  8512  ltsub1dd  8513  ltsub2dd  8514  leadd1dd  8515  leadd2dd  8516  lesub1dd  8517  lesub2dd  8518  recexre  8534  apreap  8543  ltmul1a  8547  reapmul1  8551  cru  8558  apreim  8559  mulge0  8575  leltap  8581  negap0d  8587  ltleap  8588  ltapd  8594  ap0gt0  8596  ap0gt0d  8597  mulcanapad  8619  mulcanap2ad  8620  eqnegad  8690  diveqap0d  8753  diveqap1d  8754  divap1d  8757  rec11apd  8767  div11apd  8787  div2subap  8793  recgt0  8806  prodgt0  8808  lemul1a  8814  lemulge12  8823  lt2msq1  8841  lediv12a  8850  recreclt  8856  nn1suc  8937  nnnlt1  8944  nn2ge  8951  nn1gt1  8952  nnrecl  9173  nn0nlt0  9201  elnn0z  9265  nn0negleid  9320  elz2  9323  nn0n0n1ge2b  9331  nnm1ge0  9338  nn0ge0div  9339  zextle  9343  suprzclex  9350  nn0ind-raph  9369  zindd  9370  uzneg  9545  eluzadd  9555  eluzsub  9556  uzm1  9557  uz3m2nn  9572  supminfex  9596  infregelbex  9597  nn01to3  9616  ltrec1d  9716  lerec2d  9717  ledivdivd  9721  divge1  9722  ltmul1dd  9751  ltmul2dd  9752  ltdiv1dd  9753  lediv1dd  9754  ltdiv23d  9756  lediv23d  9757  nn0ledivnn  9766  addlelt  9767  xrlelttr  9805  xrltletr  9806  xaddass2  9869  xltadd1  9875  xlt2add  9879  ixxdisj  9902  icoshftf1o  9990  icodisj  9991  lincmb01cmp  10002  iccf1o  10003  uzsubsubfz  10046  fzdisj  10051  fzopth  10060  fznatpl1  10075  fzsuc2  10078  fzp1disj  10079  fzrev2i  10085  uzdisj  10092  fseq1p1m1  10093  fzm1  10099  fzneuz  10100  fzp1nel  10103  fzrevral  10104  fznn0sub2  10127  fz0fzdiffz0  10129  difelfzle  10133  difelfznle  10134  nn0disj  10137  fzonnsub  10168  fzodisj  10177  fzouzdisj  10179  eluzgtdifelfzo  10196  ubmelfzo  10199  fzonn0p1p1  10212  ubmelm1fzo  10225  fzostep1  10236  exfzdc  10239  subfzo0  10241  qtri3or  10242  exbtwnzlemex  10249  rebtwn2z  10254  qbtwnrelemcalc  10255  qbtwnre  10256  qavgle  10258  apbtwnz  10273  flid  10283  flqwordi  10287  flqmulnn0  10298  flhalf  10301  flltdivnn0lt  10303  fldiv4p1lem1div2  10304  intfracq  10319  flqdiv  10320  flqpmodeq  10326  modqmulnn  10341  mulqaddmodid  10363  modqmuladdim  10366  modqmuladdnn0  10367  m1modge3gt1  10370  q2submod  10384  modaddmodup  10386  modqsubdir  10392  modqeqmodmin  10393  modfzo0difsn  10394  uzennn  10435  uzsinds  10441  monoord2  10476  ser3mono  10477  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemqf1o  10492  iseqf1olemqk  10493  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1olemp  10501  ser3le  10517  exp3val  10521  expnegap0  10527  expgt1  10557  ltexp2a  10571  le2sq2  10595  nnlesq  10623  qsqeqor  10630  bernneq  10640  expnbnd  10643  expnlbnd  10644  expnlbnd2  10645  expeq0d  10649  sq11d  10686  nn0ltexp2  10688  expcand  10696  nn0opthd  10701  facdiv  10717  faclbnd6  10723  facubnd  10724  facavg  10725  bcval4  10731  bcp1nk  10741  bcval5  10742  bcpasc  10745  hashennnuni  10758  isfinite4im  10771  hashnncl  10774  hashunlem  10783  fiprsshashgt1  10796  hashfzp1  10803  zfz1isolemiso  10818  seq3coll  10821  seq3shft  10846  cjth  10854  cjdivap  10917  cjne0d  10955  cjap0d  10956  cvg1nlemcxze  10990  cvg1nlemcau  10992  cvg1nlemres  10993  recvguniq  11003  resqrexlemover  11018  resqrexlemdecn  11020  resqrexlemlo  11021  resqrexlemcalc2  11023  resqrexlemcalc3  11024  resqrexlemnmsq  11025  resqrexlemnm  11026  resqrexlemcvg  11027  resqrexlemglsq  11030  resqrexlemga  11031  leabs  11082  absrele  11091  nn0abscl  11093  ltabs  11095  abslt  11096  absle  11097  abstri  11112  amgm2  11126  sqr11d  11181  abs00d  11194  maxabsle  11212  maxabslemlub  11215  maxleastlt  11223  maxltsup  11226  2zsupmax  11233  minmax  11237  2zinfmin  11250  xrmaxleim  11251  xrmaxiflemlub  11255  xrmaxiflemcom  11256  xrmaxiflemval  11257  xrmaxleastlt  11263  xrmaxltsup  11265  xrmaxaddlem  11267  xrmaxadd  11268  xrminmax  11272  xrmin1inf  11274  xrmin2inf  11275  xrmineqinf  11276  climi  11294  reccn2ap  11320  climge0  11332  climle  11341  climserle  11352  climrecvg1n  11355  fz1f1o  11382  summodclem3  11387  summodclem2a  11388  summodc  11390  fisumss  11399  fsum0diaglem  11447  mptfzshft  11449  fsumrev  11450  fisum0diag2  11454  fsumlessfi  11467  fsumle  11470  fsumlt  11471  isumsplit  11498  isumrpcl  11501  expcnvap0  11509  geosergap  11513  pwm1geoserap1  11515  absgtap  11517  geolim  11518  geolim2  11519  georeclim  11520  geoisumr  11525  geoisum1c  11527  cvgratnnlembern  11530  cvgratnnlemseq  11533  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratnn  11538  cvgratz  11539  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodmodclem2a  11583  prodmodc  11585  zproddc  11586  fprodntrivap  11591  fprodf1o  11595  fprodssdc  11597  fprodsplitdc  11603  fprodrev  11626  fprodmodd  11648  efcllemp  11665  ege2le3  11678  eftlcvg  11694  eftlub  11697  efltim  11705  eflegeo  11708  tanaddap  11746  sinbnd  11759  cosbnd  11760  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  cos01gt0  11769  cos12dec  11774  eirraplem  11783  zdvdsdc  11818  dvdstr  11834  dvdsadd2b  11846  dvdslelemd  11848  divconjdvds  11854  alzdvds  11859  dvdsext  11860  fzm1ndvds  11861  fzo0dvdseq  11862  zeo3  11872  even2n  11878  mod2eq1n2dvds  11883  nn0ehalf  11907  nnehalf  11908  nno  11910  nn0oddm1d2  11913  divalglemnqt  11924  divalglemex  11926  divalglemeuneg  11927  divalg2  11930  divalgmod  11931  flodddiv4t2lthalf  11941  zsupcllemstep  11945  infssuzex  11949  zsupssdc  11954  dvdsbnd  11956  gcdsupex  11957  gcdsupcl  11958  gcddvds  11963  divgcdz  11971  divgcdnn  11975  gcd0id  11979  gcdneg  11982  gcd1  11987  dvdsgcdidd  11994  bezoutlemnewy  11996  bezoutlemstep  11997  bezoutlemmo  12006  bezoutlemsup  12009  dfgcd3  12010  bezout  12011  dfgcd2  12014  mulgcd  12016  sqgcd  12029  dvdssqlem  12030  bezoutr1  12033  uzwodc  12037  lcmval  12062  lcmcllem  12066  dvdslcm  12068  lcmgcdlem  12076  lcmdvds  12078  lcmgcdeq  12082  ncoprmgcdne1b  12088  mulgcddvds  12093  rpmulgcd2  12094  qredeu  12096  rpdvds  12098  prmind2  12119  nprm  12122  dvdsnprmd  12124  isprm5lem  12140  isprm5  12141  divgcdodd  12142  isprm6  12146  prmexpb  12150  pw2dvds  12165  pw2dvdseulemle  12166  oddpwdclemdc  12172  sqne2sq  12176  znege1  12177  sqrt2irraplemnn  12178  divnumden  12195  divdenle  12196  qden1elz  12204  nn0sqrtelqelz  12205  hashdvds  12220  crth  12223  phimullem  12224  eulerthlemfi  12227  eulerthlemh  12230  eulerthlemth  12231  eulerth  12232  prmdiv  12234  prmdiveq  12235  hashgcdlem  12237  phisum  12239  odzcllem  12241  odzdvds  12244  odzphi  12245  oddprm  12258  pythagtriplem3  12266  pythagtriplem4  12267  pythagtriplem10  12268  pythagtriplem11  12273  pythagtriplem13  12275  pythagtriplem19  12281  pcprendvds  12289  pcprendvds2  12290  pcpre1  12291  pcpremul  12292  pceulem  12293  pceu  12294  pczpre  12296  pcmul  12300  pcdiv  12301  pcqmul  12302  pcqdiv  12306  pcexp  12308  pcidlem  12321  pcneg  12323  pcdvdstr  12325  pcgcd1  12326  pc2dvds  12328  dvdsprmpweq  12333  dvdsprmpweqle  12335  pcaddlem  12337  pcadd  12338  pcmpt  12340  fldivp1  12345  pcfaclem  12346  pcfac  12347  pcbc  12348  qexpz  12349  oddprmdvds  12351  pockthlem  12353  pockthg  12354  infpnlem2  12357  1arith  12364  4sqlem9  12383  4sqlem10  12384  oddennn  12392  ennnfonelemk  12400  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemrnh  12416  ennnfonelemen  12421  ennnfonelemim  12424  ctinfomlemom  12427  ctiunctlemf  12438  ssnnctlemct  12446  nninfdclemcl  12448  nninfdclemp1  12450  nninfdclemlt  12451  unbendc  12454  mgmb1mgm1  12786  mgm1  12788  mgmidsssn0  12802  sgrp1  12815  sgrpidmndm  12820  ismndd  12837  mhmpropd  12856  isgrpd2e  12895  grpidd2  12913  isgrpinv  12925  grpinvinv  12936  grpidssd  12945  grpinvssd  12946  mulgval  12985  mulgfng  12986  mulgnegnn  12992  subg0  13038  issubg4m  13051  nsgconj  13064  1nsgtrivd  13077  eqgen  13084  eqgcpbl  13085  issrgid  13162  srg1zr  13168  ringcl  13194  isringid  13206  ringcom  13212  ringpropd  13215  ringlz  13220  ringrz  13221  ring1  13234  opprring  13247  dvdsrcld  13264  unitcld  13275  unitmulcl  13280  unitgrp  13283  unitnegcl  13297  subrgugrp  13359  aprsym  13372  islmodd  13381  ntridm  13596  ntrtop  13598  ntrcls0  13601  ntr0  13604  isopn3i  13605  neiss2  13612  opnneiss  13628  topssnei  13632  cnpf2  13677  icnpimaex  13681  lmcvg  13687  iscnp4  13688  cncnp  13700  cnptopresti  13708  lmfss  13714  lmtopcnp  13720  hmeores  13785  bldisj  13871  xblss2ps  13874  xblss2  13875  blhalf  13878  blssps  13897  blss  13898  ssblex  13901  blpnfctr  13909  xmetresbl  13910  mopni2  13953  bdxmet  13971  bdbl  13973  xmetxpbl  13978  metcnpi  13985  metcnpi2  13986  tgioo  14016  rescncf  14038  mulcncflem  14060  cnopnap  14064  dedekindeulemuub  14065  dedekindeulemloc  14067  dedekindeulemlu  14069  dedekindeu  14071  dedekindicclemuub  14074  dedekindicclemloc  14076  dedekindicclemlu  14078  dedekindicclemicc  14080  dedekindicc  14081  ivthinclemlopn  14084  ivthinclemuopn  14086  ivthdec  14092  limcimolemlt  14103  cnplimcim  14106  cnplimclemr  14108  limccnpcntop  14114  limccnp2cntop  14116  limccoap  14117  dvfgg  14127  dvidlemap  14130  dvaddxxbr  14135  dvmulxxbr  14136  dvaddxx  14137  dvmulxx  14138  dviaddf  14139  dvimulf  14140  dvcoapbr  14141  dvcjbr  14142  dvcj  14143  dvrecap  14147  dvmptclx  14150  dveflem  14157  reeff1oleme  14163  eflt  14166  sin0pilem1  14172  pilem3  14174  cosq14gt0  14223  coseq0negpitopi  14227  tangtx  14229  coskpi  14239  cosordlem  14240  cosq34lt1  14241  relogef  14255  logrpap0d  14269  rplogcl  14270  logge0  14271  logdivlti  14272  cxplt3  14310  rpabscxpbnd  14329  lgslem1  14371  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  lgsvalmod  14390  lgsfcl3  14392  lgsmod  14397  lgsdirprm  14405  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  bj-charfunr  14532  pwf1oexmid  14719  subctctexmid  14720  pw1nct  14722  nnsf  14724  peano4nninf  14725  nninfsellemeq  14733  cvgcmp2nlemabs  14750  iooref1o  14752  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  trirec0  14762  apdifflemf  14764  apdifflemr  14765  apdiff  14766  iswomninnlem  14767  redcwlpo  14773  redc0  14775  reap0  14776  nconstwlpolemgt0  14781  neapmkvlem  14784  ltlenmkv  14787  supfz  14788  inffz  14789