Theorem mpbid 145

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpbii  146  annimdc  878  mpbi2and  884  bilukdc  1327  equs5or  1751  eqtrd  2113  eleqtrd  2157  neeqtrd  2273  3netr3d  2277  rexlimd2  2475  ceqsalt  2625  vtoclgft  2649  vtoclegft  2670  elrab3t  2748  eueq2dc  2765  sbceq1dd  2821  csbiedf  2943  sseqtrd  3035  3sstr3d  3041  snssd  3530  dfnfc2  3619  breqtrd  3809  3brtr3d  3814  csbexga  3906  reuhypd  4221  reg2exmidlema  4277  elirr  4284  en2lp  4297  onsucuni2  4307  finds  4341  iota4  4905  iota4an  4906  funimaexglem  5002  fneu  5023  fco2  5077  fssres2  5087  fresin  5088  feu  5092  f1orescnv  5162  resdif  5168  funcocnv2  5171  f1oprg  5188  fvelrnb  5242  fimacnv  5317  f1oresrab  5350  fsn2  5358  xpsng  5359  fnressn  5370  fsnunf  5383  foeqcnvco  5450  isores1  5474  isoini2  5478  riota5f  5512  riotass2  5514  riotass  5515  ovmpt2dxf  5646  elopabi  5841  cnvf1o  5866  smores3  5931  tfrlemisucaccv  5962  nnsucsssuc  6094  erref  6149  iserd  6155  swoer  6157  swoord1  6158  swoord2  6159  erth  6173  erthi  6175  eroveu  6220  fndmeng  6312  phplem4  6341  phplem4on  6353  fidifsnen  6355  dif1en  6364  fisbth  6367  diffisn  6377  ac6sfi  6379  en2eqpr  6380  unsnfidcex  6385  unsnfidcel  6386  eqsupti  6409  supisoti  6423  ordiso2  6446  dfplpq2  6544  ltanqi  6592  ltmnqi  6593  ltaddnq  6597  subhalfnqq  6604  ltbtwnnqq  6605  archnqq  6607  prarloclemarch2  6609  enq0sym  6622  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  nnnq0lem1  6636  distrnq0  6649  prarloclemlt  6683  prarloclemn  6689  prarloclemcalc  6692  genplt2i  6700  addnqprllem  6717  addnqprulem  6718  addlocprlemgt  6724  appdivnq  6753  prmuloc2  6757  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemru  6802  prplnqu  6810  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemladdfu  6844  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  archrecnq  6853  archrecpr  6854  caucvgprlemk  6855  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprprlemk  6873  caucvgprprlemnkeqj  6880  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlem1  6899  caucvgprprlem2  6900  prsrlem1  6919  addgt0sr  6952  srpospr  6959  prsrriota  6964  caucvgsrlemgt1  6971  caucvgsrlemoffgt1  6975  caucvgsr  6978  recriota  7056  lelttr  7199  ltletr  7200  ltnsymd  7229  lensymd  7231  cnegexlem3  7285  cnegex2  7287  addcanad  7294  addcan2ad  7295  negcon1ad  7414  negne0d  7417  negrebd  7418  subeq0d  7427  subne0ad  7430  neg11d  7431  subcand  7460  subcan2d  7461  ltadd2  7523  ltadd2dd  7526  add20  7578  ltnegcon1d  7625  ltnegcon2d  7626  lenegcon1d  7627  lenegcon2d  7628  subled  7648  lesubd  7649  ltsub23d  7650  ltsub13d  7651  ltadd1dd  7656  ltsub1dd  7657  ltsub2dd  7658  leadd1dd  7659  leadd2dd  7660  lesub1dd  7661  lesub2dd  7662  recexre  7678  apreap  7687  ltmul1a  7691  reapmul1  7695  cru  7702  apreim  7703  mulge0  7719  leltap  7724  ltleap  7730  ltapd  7736  ap0gt0  7738  ap0gt0d  7739  subap0d  7740  mulcanapad  7753  mulcanap2ad  7754  eqnegad  7822  diveqap0d  7884  diveqap1d  7885  divap1d  7888  rec11apd  7898  div11apd  7917  recgt0  7928  prodgt0  7930  lemul1a  7936  lemulge12  7945  lt2msq1  7963  lediv12a  7972  recreclt  7978  nn1suc  8058  nnnlt1  8065  nn2ge  8071  nn1gt1  8072  nnrecl  8286  nn0nlt0  8314  elnn0z  8364  elz2  8419  nn0n0n1ge2b  8427  nnm1ge0  8433  nn0ge0div  8434  zextle  8438  suprzclex  8445  nn0ind-raph  8464  zindd  8465  uzneg  8637  eluzadd  8647  eluzsub  8648  uzm1  8649  uz3m2nn  8661  supminfex  8685  nn01to3  8702  ltrec1d  8794  lerec2d  8795  ledivdivd  8799  divge1  8800  ltmul1dd  8829  ltmul2dd  8830  ltdiv1dd  8831  lediv1dd  8832  ltdiv23d  8834  lediv23d  8835  nn0ledivnn  8838  addlelt  8839  xrlelttr  8876  xrltletr  8877  ixxdisj  8926  icoshftf1o  9013  icodisj  9014  lincmb01cmp  9025  iccf1o  9026  uzsubsubfz  9066  fzdisj  9071  fzopth  9079  fznatpl1  9093  fzsuc2  9096  fzp1disj  9097  fzrev2i  9103  uzdisj  9110  fseq1p1m1  9111  fzm1  9117  fzneuz  9118  fzp1nel  9121  fzrevral  9122  fznn0sub2  9139  fz0fzdiffz0  9141  difelfzle  9145  difelfznle  9146  nn0disj  9148  fzonnsub  9178  fzodisj  9187  fzouzdisj  9189  eluzgtdifelfzo  9206  ubmelfzo  9209  fzonn0p1p1  9222  ubmelm1fzo  9235  fzostep1  9246  exfzdc  9249  subfzo0  9251  qtri3or  9252  qbtwnzlemex  9259  rebtwn2z  9263  qbtwnrelemcalc  9264  qbtwnre  9265  qavgle  9267  flid  9286  flqwordi  9290  flqmulnn0  9301  flhalf  9304  flltdivnn0lt  9306  fldiv4p1lem1div2  9307  intfracq  9322  flqdiv  9323  flqpmodeq  9329  modqmulnn  9344  mulqaddmodid  9366  modqmuladdim  9369  modqmuladdnn0  9370  m1modge3gt1  9373  q2submod  9387  modaddmodup  9389  modqsubdir  9395  modqeqmodmin  9396  modfzo0difsn  9397  uzsinds  9428  monoord2  9456  isermono  9457  serile  9474  expival  9478  expnegap0  9484  expgt1  9514  ltexp2a  9528  le2sq2  9551  nnlesq  9578  bernneq  9593  expnbnd  9596  expnlbnd  9597  expnlbnd2  9598  expeq0d  9601  sq11d  9638  expcand  9645  nn0opthd  9649  facdiv  9665  faclbnd6  9671  facubnd  9672  facavg  9673  bcval4  9679  bcp1nk  9689  ibcval5  9690  bcpasc  9693  cjth  9733  cjdivap  9796  cjne0d  9834  cjap0d  9835  cvg1nlemcxze  9868  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnmsq  9903  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemglsq  9908  resqrexlemga  9909  leabs  9960  absrele  9969  nn0abscl  9971  ltabs  9973  abslt  9974  absle  9975  abstri  9990  amgm2  10004  sqr11d  10059  abs00d  10072  maxabsle  10090  maxabslemlub  10093  maxleastlt  10101  maxltsup  10104  minmax  10112  climi  10126  climge0  10163  climle  10172  climserile  10183  climrecvg1n  10185  zdvdsdc  10216  dvdstr  10232  dvdsadd2b  10242  dvdslelemd  10243  divconjdvds  10249  alzdvds  10254  dvdsext  10255  fzm1ndvds  10256  fzo0dvdseq  10257  zeo3  10267  even2n  10273  mod2eq1n2dvds  10279  nn0ehalf  10303  nnehalf  10304  nno  10306  nn0oddm1d2  10309  divalglemnqt  10320  divalglemex  10322  divalglemeuneg  10323  divalg2  10326  divalgmod  10327  flodddiv4t2lthalf  10337  zsupcllemstep  10341  infssuzex  10345  dvdsbnd  10348  gcdsupex  10349  gcdsupcl  10350  gcddvds  10355  divgcdz  10363  divgcdnn  10366  gcd0id  10370  gcdneg  10373  gcd1  10378  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmo  10395  bezoutlemsup  10398  dfgcd3  10399  bezout  10400  dfgcd2  10403  mulgcd  10405  sqgcd  10418  dvdssqlem  10419  bezoutr1  10422  lcmval  10445  lcmcllem  10449  dvdslcm  10451  lcmgcdlem  10459  lcmdvds  10461  lcmgcdeq  10465  ncoprmgcdne1b  10471  mulgcddvds  10476  rpmulgcd2  10477  qredeu  10479  rpdvds  10481  prmind2  10502  nprm  10505  dvdsnprmd  10507  divgcdodd  10522  isprm6  10526  prmexpb  10530  pw2dvds  10544  pw2dvdseulemle  10545  oddpwdclemdc  10551  sqne2sq  10555  znege1  10556  sqrt2irraplemnn  10557