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  921  mpbi2and  927  bilukdc  1374  equs5or  1802  eqtrd  2172  eleqtrd  2218  neeqtrd  2336  3netr3d  2340  rexlimd2  2547  ceqsalt  2712  vtoclgft  2736  vtoclegft  2758  elrab3t  2839  eueq2dc  2857  sbceq1dd  2915  csbiedf  3040  sseqtrd  3135  3sstr3d  3141  ifbothdadc  3503  snssd  3665  dfnfc2  3754  breqdi  3944  breqtrd  3954  3brtr3d  3959  csbexga  4056  reuhypd  4392  reg2exmidlema  4449  elirr  4456  en2lp  4469  onsucuni2  4479  finds  4514  iota4  5106  iota4an  5107  funimaexglem  5206  fneu  5227  fco2  5289  fssres2  5300  fresin  5301  feu  5305  f1orescnv  5383  resdif  5389  funcocnv2  5392  f1oprg  5411  fvelrnb  5469  fimacnv  5549  f1oresrab  5585  fsn2  5594  xpsng  5595  fnressn  5606  fsnunf  5620  foeqcnvco  5691  isores1  5715  isoini2  5720  riota5f  5754  riotass2  5756  riotass  5757  ovmpodxf  5896  elopabi  6093  cnvf1o  6122  smores3  6190  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  rdgon  6283  frecabcl  6296  frecsuclem  6303  nnsucsssuc  6388  nnsucuniel  6391  erref  6449  iserd  6455  swoer  6457  swoord1  6458  swoord2  6459  erth  6473  erthi  6475  eroveu  6520  pmresg  6570  mapsn  6584  fndmeng  6704  xpen  6739  phplem4  6749  phplem4on  6761  fidifsnen  6764  dif1en  6773  dif1enen  6774  fisbth  6777  diffisn  6787  ac6sfi  6792  fimax2gtri  6795  en2eqpr  6801  unsnfidcex  6808  unsnfidcel  6809  fiintim  6817  fidcenumlemrks  6841  elfi2  6860  elfir  6861  fiuni  6866  fifo  6868  eqsupti  6883  supisoti  6897  ordiso2  6920  casef  6973  difinfsnlem  6984  ctmlemr  6993  ctssdccl  6996  enumct  7000  enomnilem  7010  exmidomni  7014  fodjum  7018  fodjuomnilemres  7020  mkvprop  7032  acfun  7063  ccfunen  7079  dfplpq2  7162  ltanqi  7210  ltmnqi  7211  ltaddnq  7215  subhalfnqq  7222  ltbtwnnqq  7223  archnqq  7225  prarloclemarch2  7227  enq0sym  7240  enq0ref  7241  enq0tr  7242  nqnq0pi  7246  nnnq0lem1  7254  distrnq0  7267  prarloclemlt  7301  prarloclemn  7307  prarloclemcalc  7310  genplt2i  7318  addnqprllem  7335  addnqprulem  7336  addlocprlemgt  7342  appdivnq  7371  prmuloc2  7375  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemru  7420  prplnqu  7428  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemladdfu  7462  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  archrecnq  7471  archrecpr  7472  caucvgprlemk  7473  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgprprlemk  7491  caucvgprprlemnkeqj  7498  caucvgprprlemnbj  7501  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemexbt  7514  caucvgprprlemexb  7515  caucvgprprlem1  7517  caucvgprprlem2  7518  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  prsrlem1  7550  addgt0sr  7583  srpospr  7591  prsrriota  7596  caucvgsrlemgt1  7603  caucvgsrlemoffgt1  7607  caucvgsr  7610  mappsrprg  7612  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  recriota  7698  axsuploc  7837  lelttr  7852  ltletr  7853  ltnsymd  7882  lensymd  7884  cnegexlem3  7939  cnegex2  7941  addcanad  7948  addcan2ad  7949  negcon1ad  8068  negne0d  8071  negrebd  8072  subeq0d  8081  subne0ad  8084  neg11d  8085  subcand  8114  subcan2d  8115  ltadd2  8181  ltadd2dd  8184  add20  8236  ltnegcon1d  8287  ltnegcon2d  8288  lenegcon1d  8289  lenegcon2d  8290  subled  8310  lesubd  8311  ltsub23d  8312  ltsub13d  8313  ltadd1dd  8318  ltsub1dd  8319  ltsub2dd  8320  leadd1dd  8321  leadd2dd  8322  lesub1dd  8323  lesub2dd  8324  recexre  8340  apreap  8349  ltmul1a  8353  reapmul1  8357  cru  8364  apreim  8365  mulge0  8381  leltap  8387  negap0d  8393  ltleap  8394  ltapd  8400  ap0gt0  8402  ap0gt0d  8403  subap0d  8406  mulcanapad  8424  mulcanap2ad  8425  eqnegad  8494  diveqap0d  8557  diveqap1d  8558  divap1d  8561  rec11apd  8571  div11apd  8591  div2subap  8596  recgt0  8608  prodgt0  8610  lemul1a  8616  lemulge12  8625  lt2msq1  8643  lediv12a  8652  recreclt  8658  nn1suc  8739  nnnlt1  8746  nn2ge  8753  nn1gt1  8754  nnrecl  8975  nn0nlt0  9003  elnn0z  9067  elz2  9122  nn0n0n1ge2b  9130  nnm1ge0  9137  nn0ge0div  9138  zextle  9142  suprzclex  9149  nn0ind-raph  9168  zindd  9169  uzneg  9344  eluzadd  9354  eluzsub  9355  uzm1  9356  uz3m2nn  9368  supminfex  9392  nn01to3  9409  ltrec1d  9504  lerec2d  9505  ledivdivd  9509  divge1  9510  ltmul1dd  9539  ltmul2dd  9540  ltdiv1dd  9541  lediv1dd  9542  ltdiv23d  9544  lediv23d  9545  nn0ledivnn  9554  addlelt  9555  xrlelttr  9589  xrltletr  9590  xaddass2  9653  xltadd1  9659  xlt2add  9663  ixxdisj  9686  icoshftf1o  9774  icodisj  9775  lincmb01cmp  9786  iccf1o  9787  uzsubsubfz  9827  fzdisj  9832  fzopth  9841  fznatpl1  9856  fzsuc2  9859  fzp1disj  9860  fzrev2i  9866  uzdisj  9873  fseq1p1m1  9874  fzm1  9880  fzneuz  9881  fzp1nel  9884  fzrevral  9885  fznn0sub2  9905  fz0fzdiffz0  9907  difelfzle  9911  difelfznle  9912  nn0disj  9915  fzonnsub  9946  fzodisj  9955  fzouzdisj  9957  eluzgtdifelfzo  9974  ubmelfzo  9977  fzonn0p1p1  9990  ubmelm1fzo  10003  fzostep1  10014  exfzdc  10017  subfzo0  10019  qtri3or  10020  exbtwnzlemex  10027  rebtwn2z  10032  qbtwnrelemcalc  10033  qbtwnre  10034  qavgle  10036  apbtwnz  10047  flid  10057  flqwordi  10061  flqmulnn0  10072  flhalf  10075  flltdivnn0lt  10077  fldiv4p1lem1div2  10078  intfracq  10093  flqdiv  10094  flqpmodeq  10100  modqmulnn  10115  mulqaddmodid  10137  modqmuladdim  10140  modqmuladdnn0  10141  m1modge3gt1  10144  q2submod  10158  modaddmodup  10160  modqsubdir  10166  modqeqmodmin  10167  modfzo0difsn  10168  uzennn  10209  uzsinds  10215  monoord2  10250  ser3mono  10251  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  iseqf1olemqf1o  10266  iseqf1olemqk  10267  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1olemp  10275  ser3le  10291  exp3val  10295  expnegap0  10301  expgt1  10331  ltexp2a  10345  le2sq2  10368  nnlesq  10396  bernneq  10412  expnbnd  10415  expnlbnd  10416  expnlbnd2  10417  expeq0d  10420  sq11d  10457  expcand  10464  nn0opthd  10468  facdiv  10484  faclbnd6  10490  facubnd  10491  facavg  10492  bcval4  10498  bcp1nk  10508  bcval5  10509  bcpasc  10512  hashennnuni  10525  focdmex  10533  isfinite4im  10539  hashnncl  10542  hashunlem  10550  fiprsshashgt1  10563  hashfzp1  10570  zfz1isolemiso  10582  seq3coll  10585  seq3shft  10610  cjth  10618  cjdivap  10681  cjne0d  10719  cjap0d  10720  cvg1nlemcxze  10754  cvg1nlemcau  10756  cvg1nlemres  10757  recvguniq  10767  resqrexlemover  10782  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnmsq  10789  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemglsq  10794  resqrexlemga  10795  leabs  10846  absrele  10855  nn0abscl  10857  ltabs  10859  abslt  10860  absle  10861  abstri  10876  amgm2  10890  sqr11d  10945  abs00d  10958  maxabsle  10976  maxabslemlub  10979  maxleastlt  10987  maxltsup  10990  2zsupmax  10997  minmax  11001  xrmaxleim  11013  xrmaxiflemlub  11017  xrmaxiflemcom  11018  xrmaxiflemval  11019  xrmaxleastlt  11025  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrminmax  11034  xrmin1inf  11036  xrmin2inf  11037  xrmineqinf  11038  climi  11056  reccn2ap  11082  climge0  11094  climle  11103  climserle  11114  climrecvg1n  11117  fz1f1o  11144  summodclem3  11149  summodclem2a  11150  summodc  11152  fisumss  11161  fsum0diaglem  11209  mptfzshft  11211  fsumrev  11212  fisum0diag2  11216  fsumlessfi  11229  fsumle  11232  fsumlt  11233  isumsplit  11260  isumrpcl  11263  expcnvap0  11271  geosergap  11275  pwm1geoserap1  11277  absgtap  11279  geolim  11280  geolim2  11281  georeclim  11282  geoisumr  11287  geoisum1c  11289  cvgratnnlembern  11292  cvgratnnlemseq  11295  cvgratnnlemsumlt  11297  cvgratnnlemfm  11298  cvgratnnlemrate  11299  cvgratnn  11300  cvgratz  11301  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodmodclem2a  11345  prodmodc  11347  efcllemp  11364  ege2le3  11377  eftlcvg  11393  eftlub  11396  efltim  11404  eflegeo  11408  tanaddap  11446  sinbnd  11459  cosbnd  11460  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos01gt0  11469  cos12dec  11474  eirraplem  11483  zdvdsdc  11514  dvdstr  11530  dvdsadd2b  11540  dvdslelemd  11541  divconjdvds  11547  alzdvds  11552  dvdsext  11553  fzm1ndvds  11554  fzo0dvdseq  11555  zeo3  11565  even2n  11571  mod2eq1n2dvds  11576  nn0ehalf  11600  nnehalf  11601  nno  11603  nn0oddm1d2  11606  divalglemnqt  11617  divalglemex  11619  divalglemeuneg  11620  divalg2  11623  divalgmod  11624  flodddiv4t2lthalf  11634  zsupcllemstep  11638  infssuzex  11642  dvdsbnd  11645  gcdsupex  11646  gcdsupcl  11647  gcddvds  11652  divgcdz  11660  divgcdnn  11663  gcd0id  11667  gcdneg  11670  gcd1  11675  dvdsgcdidd  11682  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmo  11694  bezoutlemsup  11697  dfgcd3  11698  bezout  11699  dfgcd2  11702  mulgcd  11704  sqgcd  11717  dvdssqlem  11718  bezoutr1  11721  lcmval  11744  lcmcllem  11748  dvdslcm  11750  lcmgcdlem  11758  lcmdvds  11760  lcmgcdeq  11764  ncoprmgcdne1b  11770  mulgcddvds  11775  rpmulgcd2  11776  qredeu  11778  rpdvds  11780  prmind2  11801  nprm  11804  dvdsnprmd  11806  divgcdodd  11821  isprm6  11825  prmexpb  11829  pw2dvds  11844  pw2dvdseulemle  11845  oddpwdclemdc  11851  sqne2sq  11855  znege1  11856  sqrt2irraplemnn  11857  divnumden  11874  divdenle  11875  qden1elz  11883  nn0sqrtelqelz  11884  hashdvds  11897  crth  11900  phimullem  11901  hashgcdlem  11903  oddennn  11905  ennnfonelemk  11913  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemrnh  11929  ennnfonelemen  11934  ennnfonelemim  11937  ctinfomlemom  11940  ctiunctlemf  11951  ntridm  12295  ntrtop  12297  ntrcls0  12300  ntr0  12303  isopn3i  12304  neiss2  12311  opnneiss  12327  topssnei  12331  cnpf2  12376  icnpimaex  12380  lmcvg  12386  iscnp4  12387  cncnp  12399  cnptopresti  12407  lmfss  12413  lmtopcnp  12419  hmeores  12484  bldisj  12570  xblss2ps  12573  xblss2  12574  blhalf  12577  blssps  12596  blss  12597  ssblex  12600  blpnfctr  12608  xmetresbl  12609  mopni2  12652  bdxmet  12670  bdbl  12672  xmetxpbl  12677  metcnpi  12684  metcnpi2  12685  tgioo  12715  rescncf  12737  mulcncflem  12759  cnopnap  12763  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeu  12770  dedekindicclemuub  12773  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemicc  12779  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthdec  12791  limcimolemlt  12802  cnplimcim  12805  cnplimclemr  12807  limccnpcntop  12813  limccnp2cntop  12815  limccoap  12816  dvfgg  12826  dvidlemap  12829  dvaddxxbr  12834  dvmulxxbr  12835  dvaddxx  12836  dvmulxx  12837  dviaddf  12838  dvimulf  12839  dvcoapbr  12840  dvcjbr  12841  dvcj  12842  dvrecap  12846  dvmptclx  12849  dveflem  12855  sin0pilem1  12862  pilem3  12864  cosq14gt0  12913  coseq0negpitopi  12917  tangtx  12919  coskpi  12929  cosordlem  12930  cosq34lt1  12931  pwf1oexmid  13194  subctctexmid  13196  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfsellemeq  13210  cvgcmp2nlemabs  13227  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234  supfz  13237  inffz  13238