Theorem mpbid 146

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 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbii  147  annimdc  932  mpbi2and  938  bilukdc  1391  equs5or  1823  eqtrd  2203  eleqtrd  2249  neeqtrd  2368  3netr3d  2372  rexlimd2  2585  ceqsalt  2756  vtoclgft  2780  vtoclegft  2802  elrab3t  2885  eueq2dc  2903  sbceq1dd  2961  csbiedf  3089  sseqtrd  3185  3sstr3d  3191  ifbothdadc  3556  snssd  3723  dfnfc2  3812  breqdi  4002  breqtrd  4013  3brtr3d  4018  csbexga  4115  reuhypd  4454  reg2exmidlema  4516  elirr  4523  en2lp  4536  onsucuni2  4546  finds  4582  iota4  5176  iota4an  5177  funimaexglem  5279  fneu  5300  fco2  5362  fssres2  5373  fresin  5374  feu  5378  f1orescnv  5456  resdif  5462  funcocnv2  5465  f1oprg  5484  fvelrnb  5542  fimacnv  5622  f1oresrab  5658  fsn2  5667  xpsng  5668  fnressn  5679  fsnunf  5693  foeqcnvco  5766  isores1  5790  isoini2  5795  riota5f  5830  riotass2  5832  riotass  5833  ovmpodxf  5975  elopabi  6171  cnvf1o  6201  smores3  6269  tfrlemisucaccv  6301  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  rdgon  6362  frecabcl  6375  frecsuclem  6382  nnsucsssuc  6468  nnsucuniel  6471  erref  6529  iserd  6535  swoer  6537  swoord1  6538  swoord2  6539  erth  6553  erthi  6555  eroveu  6600  pmresg  6650  mapsn  6664  fndmeng  6784  xpen  6819  phplem4  6829  phplem4on  6841  fidifsnen  6844  dif1en  6853  dif1enen  6854  fisbth  6857  diffisn  6867  ac6sfi  6872  fimax2gtri  6875  en2eqpr  6881  unsnfidcex  6893  unsnfidcel  6894  fiintim  6902  fidcenumlemrks  6926  elfi2  6945  elfir  6946  fiuni  6951  fifo  6953  eqsupti  6969  supisoti  6983  ordiso2  7008  casef  7061  difinfsnlem  7072  ctmlemr  7081  ctssdccl  7084  enumct  7088  nnnninfeq  7100  nnnninfeq2  7101  enomnilem  7110  exmidomni  7114  fodjum  7118  fodjuomnilemres  7120  mkvprop  7130  enmkvlem  7133  enwomnilem  7141  acfun  7171  ccfunen  7213  cc2lem  7215  dfplpq2  7303  ltanqi  7351  ltmnqi  7352  ltaddnq  7356  subhalfnqq  7363  ltbtwnnqq  7364  archnqq  7366  prarloclemarch2  7368  enq0sym  7381  enq0ref  7382  enq0tr  7383  nqnq0pi  7387  nnnq0lem1  7395  distrnq0  7408  prarloclemlt  7442  prarloclemn  7448  prarloclemcalc  7451  genplt2i  7459  addnqprllem  7476  addnqprulem  7477  addlocprlemgt  7483  appdivnq  7512  prmuloc2  7516  ltexprlemopl  7550  ltexprlemopu  7552  ltexprlemru  7561  prplnqu  7569  cauappcvgprlemopl  7595  cauappcvgprlemlol  7596  cauappcvgprlemladdfu  7603  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  archrecnq  7612  archrecpr  7613  caucvgprlemk  7614  caucvgprlemnbj  7616  caucvgprlemm  7617  caucvgprlemopl  7618  caucvgprlemlol  7619  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlem1  7628  caucvgprprlemk  7632  caucvgprprlemnkeqj  7639  caucvgprprlemnbj  7642  caucvgprprlemml  7643  caucvgprprlemmu  7644  caucvgprprlemopl  7646  caucvgprprlemlol  7647  caucvgprprlemopu  7648  caucvgprprlemexbt  7655  caucvgprprlemexb  7656  caucvgprprlem1  7658  caucvgprprlem2  7659  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemub  7672  suplocexprlemlub  7673  prsrlem1  7691  addgt0sr  7724  srpospr  7732  prsrriota  7737  caucvgsrlemgt1  7744  caucvgsrlemoffgt1  7748  caucvgsr  7751  mappsrprg  7753  suplocsrlemb  7755  suplocsrlempr  7756  suplocsrlem  7757  recriota  7839  axsuploc  7979  lelttr  7995  ltletr  7996  ltnsymd  8026  lensymd  8028  cnegexlem3  8083  cnegex2  8085  addcanad  8092  addcan2ad  8093  negcon1ad  8212  negne0d  8215  negrebd  8216  subeq0d  8225  subne0ad  8228  neg11d  8229  subcand  8258  subcan2d  8259  ltadd2  8325  ltadd2dd  8328  add20  8380  ltnegcon1d  8431  ltnegcon2d  8432  lenegcon1d  8433  lenegcon2d  8434  subled  8454  lesubd  8455  ltsub23d  8456  ltsub13d  8457  ltadd1dd  8462  ltsub1dd  8463  ltsub2dd  8464  leadd1dd  8465  leadd2dd  8466  lesub1dd  8467  lesub2dd  8468  recexre  8484  apreap  8493  ltmul1a  8497  reapmul1  8501  cru  8508  apreim  8509  mulge0  8525  leltap  8531  negap0d  8537  ltleap  8538  ltapd  8544  ap0gt0  8546  ap0gt0d  8547  mulcanapad  8568  mulcanap2ad  8569  eqnegad  8638  diveqap0d  8701  diveqap1d  8702  divap1d  8705  rec11apd  8715  div11apd  8735  div2subap  8741  recgt0  8753  prodgt0  8755  lemul1a  8761  lemulge12  8770  lt2msq1  8788  lediv12a  8797  recreclt  8803  nn1suc  8884  nnnlt1  8891  nn2ge  8898  nn1gt1  8899  nnrecl  9120  nn0nlt0  9148  elnn0z  9212  nn0negleid  9267  elz2  9270  nn0n0n1ge2b  9278  nnm1ge0  9285  nn0ge0div  9286  zextle  9290  suprzclex  9297  nn0ind-raph  9316  zindd  9317  uzneg  9492  eluzadd  9502  eluzsub  9503  uzm1  9504  uz3m2nn  9519  supminfex  9543  infregelbex  9544  nn01to3  9563  ltrec1d  9661  lerec2d  9662  ledivdivd  9666  divge1  9667  ltmul1dd  9696  ltmul2dd  9697  ltdiv1dd  9698  lediv1dd  9699  ltdiv23d  9701  lediv23d  9702  nn0ledivnn  9711  addlelt  9712  xrlelttr  9750  xrltletr  9751  xaddass2  9814  xltadd1  9820  xlt2add  9824  ixxdisj  9847  icoshftf1o  9935  icodisj  9936  lincmb01cmp  9947  iccf1o  9948  uzsubsubfz  9990  fzdisj  9995  fzopth  10004  fznatpl1  10019  fzsuc2  10022  fzp1disj  10023  fzrev2i  10029  uzdisj  10036  fseq1p1m1  10037  fzm1  10043  fzneuz  10044  fzp1nel  10047  fzrevral  10048  fznn0sub2  10071  fz0fzdiffz0  10073  difelfzle  10077  difelfznle  10078  nn0disj  10081  fzonnsub  10112  fzodisj  10121  fzouzdisj  10123  eluzgtdifelfzo  10140  ubmelfzo  10143  fzonn0p1p1  10156  ubmelm1fzo  10169  fzostep1  10180  exfzdc  10183  subfzo0  10185  qtri3or  10186  exbtwnzlemex  10193  rebtwn2z  10198  qbtwnrelemcalc  10199  qbtwnre  10200  qavgle  10202  apbtwnz  10217  flid  10227  flqwordi  10231  flqmulnn0  10242  flhalf  10245  flltdivnn0lt  10247  fldiv4p1lem1div2  10248  intfracq  10263  flqdiv  10264  flqpmodeq  10270  modqmulnn  10285  mulqaddmodid  10307  modqmuladdim  10310  modqmuladdnn0  10311  m1modge3gt1  10314  q2submod  10328  modaddmodup  10330  modqsubdir  10336  modqeqmodmin  10337  modfzo0difsn  10338  uzennn  10379  uzsinds  10385  monoord2  10420  ser3mono  10421  iseqf1olemqcl  10429  iseqf1olemnab  10431  iseqf1olemab  10432  iseqf1olemqf1o  10436  iseqf1olemqk  10437  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  seq3f1olemp  10445  ser3le  10461  exp3val  10465  expnegap0  10471  expgt1  10501  ltexp2a  10515  le2sq2  10538  nnlesq  10566  qsqeqor  10573  bernneq  10583  expnbnd  10586  expnlbnd  10587  expnlbnd2  10588  expeq0d  10592  sq11d  10629  nn0ltexp2  10631  expcand  10638  nn0opthd  10643  facdiv  10659  faclbnd6  10665  facubnd  10666  facavg  10667  bcval4  10673  bcp1nk  10683  bcval5  10684  bcpasc  10687  hashennnuni  10700  focdmex  10708  isfinite4im  10714  hashnncl  10717  hashunlem  10726  fiprsshashgt1  10739  hashfzp1  10746  zfz1isolemiso  10761  seq3coll  10764  seq3shft  10789  cjth  10797  cjdivap  10860  cjne0d  10898  cjap0d  10899  cvg1nlemcxze  10933  cvg1nlemcau  10935  cvg1nlemres  10936  recvguniq  10946  resqrexlemover  10961  resqrexlemdecn  10963  resqrexlemlo  10964  resqrexlemcalc2  10966  resqrexlemcalc3  10967  resqrexlemnmsq  10968  resqrexlemnm  10969  resqrexlemcvg  10970  resqrexlemglsq  10973  resqrexlemga  10974  leabs  11025  absrele  11034  nn0abscl  11036  ltabs  11038  abslt  11039  absle  11040  abstri  11055  amgm2  11069  sqr11d  11124  abs00d  11137  maxabsle  11155  maxabslemlub  11158  maxleastlt  11166  maxltsup  11169  2zsupmax  11176  minmax  11180  2zinfmin  11193  xrmaxleim  11194  xrmaxiflemlub  11198  xrmaxiflemcom  11199  xrmaxiflemval  11200  xrmaxleastlt  11206  xrmaxltsup  11208  xrmaxaddlem  11210  xrmaxadd  11211  xrminmax  11215  xrmin1inf  11217  xrmin2inf  11218  xrmineqinf  11219  climi  11237  reccn2ap  11263  climge0  11275  climle  11284  climserle  11295  climrecvg1n  11298  fz1f1o  11325  summodclem3  11330  summodclem2a  11331  summodc  11333  fisumss  11342  fsum0diaglem  11390  mptfzshft  11392  fsumrev  11393  fisum0diag2  11397  fsumlessfi  11410  fsumle  11413  fsumlt  11414  isumsplit  11441  isumrpcl  11444  expcnvap0  11452  geosergap  11456  pwm1geoserap1  11458  absgtap  11460  geolim  11461  geolim2  11462  georeclim  11463  geoisumr  11468  geoisum1c  11470  cvgratnnlembern  11473  cvgratnnlemseq  11476  cvgratnnlemsumlt  11478  cvgratnnlemfm  11479  cvgratnnlemrate  11480  cvgratnn  11481  cvgratz  11482  mertenslemub  11484  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  prodmodclem2a  11526  prodmodc  11528  zproddc  11529  fprodntrivap  11534  fprodf1o  11538  fprodssdc  11540  fprodsplitdc  11546  fprodrev  11569  fprodmodd  11591  efcllemp  11608  ege2le3  11621  eftlcvg  11637  eftlub  11640  efltim  11648  eflegeo  11651  tanaddap  11689  sinbnd  11702  cosbnd  11703  sin01bnd  11707  cos01bnd  11708  sin01gt0  11711  cos01gt0  11712  cos12dec  11717  eirraplem  11726  zdvdsdc  11761  dvdstr  11777  dvdsadd2b  11789  dvdslelemd  11790  divconjdvds  11796  alzdvds  11801  dvdsext  11802  fzm1ndvds  11803  fzo0dvdseq  11804  zeo3  11814  even2n  11820  mod2eq1n2dvds  11825  nn0ehalf  11849  nnehalf  11850  nno  11852  nn0oddm1d2  11855  divalglemnqt  11866  divalglemex  11868  divalglemeuneg  11869  divalg2  11872  divalgmod  11873  flodddiv4t2lthalf  11883  zsupcllemstep  11887  infssuzex  11891  zsupssdc  11896  dvdsbnd  11898  gcdsupex  11899  gcdsupcl  11900  gcddvds  11905  divgcdz  11913  divgcdnn  11917  gcd0id  11921  gcdneg  11924  gcd1  11929  dvdsgcdidd  11936  bezoutlemnewy  11938  bezoutlemstep  11939  bezoutlemmo  11948  bezoutlemsup  11951  dfgcd3  11952  bezout  11953  dfgcd2  11956  mulgcd  11958  sqgcd  11971  dvdssqlem  11972  bezoutr1  11975  uzwodc  11979  lcmval  12004  lcmcllem  12008  dvdslcm  12010  lcmgcdlem  12018  lcmdvds  12020  lcmgcdeq  12024  ncoprmgcdne1b  12030  mulgcddvds  12035  rpmulgcd2  12036  qredeu  12038  rpdvds  12040  prmind2  12061  nprm  12064  dvdsnprmd  12066  isprm5lem  12082  isprm5  12083  divgcdodd  12084  isprm6  12088  prmexpb  12092  pw2dvds  12107  pw2dvdseulemle  12108  oddpwdclemdc  12114  sqne2sq  12118  znege1  12119  sqrt2irraplemnn  12120  divnumden  12137  divdenle  12138  qden1elz  12146  nn0sqrtelqelz  12147  hashdvds  12162  crth  12165  phimullem  12166  eulerthlemfi  12169  eulerthlemh  12172  eulerthlemth  12173  eulerth  12174  prmdiv  12176  prmdiveq  12177  hashgcdlem  12179  phisum  12181  odzcllem  12183  odzdvds  12186  odzphi  12187  oddprm  12200  pythagtriplem3  12208  pythagtriplem4  12209  pythagtriplem10  12210  pythagtriplem11  12215  pythagtriplem13  12217  pythagtriplem19  12223  pcprendvds  12231  pcprendvds2  12232  pcpre1  12233  pcpremul  12234  pceulem  12235  pceu  12236  pczpre  12238  pcmul  12242  pcdiv  12243  pcqmul  12244  pcqdiv  12248  pcexp  12250  pcidlem  12263  pcneg  12265  pcdvdstr  12267  pcgcd1  12268  pc2dvds  12270  dvdsprmpweq  12275  dvdsprmpweqle  12277  pcaddlem  12279  pcadd  12280  pcmpt  12282  fldivp1  12287  pcfaclem  12288  pcfac  12289  pcbc  12290  qexpz  12291  oddprmdvds  12293  pockthlem  12295  pockthg  12296  infpnlem2  12299  1arith  12306  4sqlem9  12325  4sqlem10  12326  oddennn  12334  ennnfonelemk  12342  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemrnh  12358  ennnfonelemen  12363  ennnfonelemim  12366  ctinfomlemom  12369  ctiunctlemf  12380  ssnnctlemct  12388  nninfdclemcl  12390  nninfdclemp1  12392  nninfdclemlt  12393  unbendc  12396  mgmb1mgm1  12609  mgm1  12611  mgmidsssn0  12625  sgrp1  12638  sgrpidmndm  12643  ismndd  12660  mhmpropd  12676  isgrpd2e  12713  grpidd2  12731  ntridm  12879  ntrtop  12881  ntrcls0  12884  ntr0  12887  isopn3i  12888  neiss2  12895  opnneiss  12911  topssnei  12915  cnpf2  12960  icnpimaex  12964  lmcvg  12970  iscnp4  12971  cncnp  12983  cnptopresti  12991  lmfss  12997  lmtopcnp  13003  hmeores  13068  bldisj  13154  xblss2ps  13157  xblss2  13158  blhalf  13161  blssps  13180  blss  13181  ssblex  13184  blpnfctr  13192  xmetresbl  13193  mopni2  13236  bdxmet  13254  bdbl  13256  xmetxpbl  13261  metcnpi  13268  metcnpi2  13269  tgioo  13299  rescncf  13321  mulcncflem  13343  cnopnap  13347  dedekindeulemuub  13348  dedekindeulemloc  13350  dedekindeulemlu  13352  dedekindeu  13354  dedekindicclemuub  13357  dedekindicclemloc  13359  dedekindicclemlu  13361  dedekindicclemicc  13363  dedekindicc  13364  ivthinclemlopn  13367  ivthinclemuopn  13369  ivthdec  13375  limcimolemlt  13386  cnplimcim  13389  cnplimclemr  13391  limccnpcntop  13397  limccnp2cntop  13399  limccoap  13400  dvfgg  13410  dvidlemap  13413  dvaddxxbr  13418  dvmulxxbr  13419  dvaddxx  13420  dvmulxx  13421  dviaddf  13422  dvimulf  13423  dvcoapbr  13424  dvcjbr  13425  dvcj  13426  dvrecap  13430  dvmptclx  13433  dveflem  13440  reeff1oleme  13446  eflt  13449  sin0pilem1  13455  pilem3  13457  cosq14gt0  13506  coseq0negpitopi  13510  tangtx  13512  coskpi  13522  cosordlem  13523  cosq34lt1  13524  relogef  13538  logrpap0d  13552  rplogcl  13553  logge0  13554  logdivlti  13555  cxplt3  13593  rpabscxpbnd  13612  lgslem1  13654  lgsval  13658  lgsfvalg  13659  lgsval2lem  13664  lgsvalmod  13673  lgsfcl3  13675  lgsmod  13680  lgsdirprm  13688  lgsdir  13689  lgsdilem2  13690  lgsdi  13691  lgsne0  13692  2sqlem3  13706  2sqlem4  13707  2sqlem8  13712  bj-charfunr  13805  pwf1oexmid  13992  subctctexmid  13994  pw1nct  13996  nnsf  13998  peano4nninf  13999  nninfsellemeq  14007  cvgcmp2nlemabs  14024  iooref1o  14026  trilpolemisumle  14030  trilpolemeq1  14032  trilpolemlt1  14033  trirec0  14036  apdifflemf  14038  apdifflemr  14039  apdiff  14040  iswomninnlem  14041  redcwlpo  14047  redc0  14049  reap0  14050  nconstwlpolemgt0  14055  neapmkvlem  14058  supfz  14060  inffz  14061