Theorem mpbii 233

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mpbii.min	⊢ 𝜓
mpbii.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbii	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpbii.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbid 232	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dedt  1084  eqcomd  2742  eqvisset  3449  vtoclg  3499  vtocl  3503  vtoclOLD  3504  vtoclf  3509  vtoclgf  3513  vtoclg1f  3514  eueq3  3657  sbc2or  3737  csbiegf  3870  un00  4385  elimhyp  4532  elimhyp2v  4533  elimhyp3v  4534  elimhyp4v  4535  elimdhyp  4537  keephyp2v  4539  keephyp3v  4540  preq12b  4793  nfopd  4833  ssex  5262  opthwiener  5468  isso2i  5576  nfimad  6034  dfrel2  6153  ordtri3or  6355  on0eqel  6448  funsng  6549  cnvresid  6577  nffvd  6852  fnbrfvb  6890  fvelrnb  6900  fvelimab  6912  funfvop  7002  fvsnun2  7138  iunpw  7725  onsucuni  7779  onuninsuci  7791  tposf12  8201  oaword1  8487  oneo  8516  nnaword1  8565  nnneo  8591  naddword1  8627  1sdom2dom  9164  inficl  9338  fipwuni  9339  infeq5i  9557  cantnflt  9593  cantnflem1  9610  cnfcom  9621  brttrcl  9634  rankidn  9746  rankr1id  9786  rankxpsuc  9806  iscard  9899  iscard2  9900  carduni  9905  cardmin2  9923  infxpenlem  9935  alephgeom  10004  cardaleph  10011  infenaleph  10013  iscard3  10015  alephsson  10022  alephfp  10030  alephval3  10032  dfac12k  10070  axdc3lem2  10373  alephval2  10495  alephreg  10505  cfpwsdom  10507  alephom  10508  axrepndlem1  10515  axunndlem1  10518  axunnd  10519  axpowndlem2  10521  axpowndlem3  10522  axpowndlem4  10523  axpownd  10524  axregndlem2  10526  axinfndlem1  10528  axinfnd  10529  axacndlem4  10533  axacndlem5  10534  axacnd  10535  gchaleph2  10595  elwina  10609  elina  10610  winaon  10611  inawina  10613  winainf  10617  winalim  10618  tskr1om2  10691  r1tskina  10705  gruina  10741  grur1a  10742  indpi  10830  nqerrel  10855  recidnq  10888  ltaddnq  10897  pncan3  11401  divcan2  11817  ltp1  11995  ltm1  11997  recreclt  12055  elnn0z  12537  nn0ind-raph  12629  fzdifsuc  13538  2tnp1ge0ge0  13788  fsuppmapnn0fiubex  13954  faclbnd5  14260  hashfun  14399  ccatalpha  14556  caucvgrlem  15635  fsumcnv  15735  fprodcnv  15948  ef01bndlem  16151  sin01gt0  16157  cos01gt0  16158  egt2lt3  16173  cnso  16214  ltoddhalfle  16330  4sqlem12  16927  funcres  17863  fuchom  17931  xpsmnd  18745  xpsgrp  19035  mulgfval  19045  mulgfvalALT  19046  nmznsg  19143  frgp0  19735  gsumval3lem2  19881  gsumval3  19882  xpsrngd  20160  xpsringd  20312  pwssplit1  21054  pzriprnglem4  21464  mvrf1  21964  psdmul  22132  ply1chr  22271  blssioo  24760  dvidlem  25882  dvcj  25917  dvrec  25922  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvlipcn  25961  dv11cn  25968  dvivthlem2  25976  lhop1lem  25980  lhop1  25981  lhop2  25982  q1peqb  26121  pserdv  26394  sinhalfpilem  26427  tangtx  26469  efabl  26514  logi  26551  logneg2  26579  gausslemma2dlem1a  27328  lgseisenlem4  27341  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  dchrisum0lem3  27482  mulogsum  27495  pntrlog2bndlem1  27540  madebday  27892  ltsp1d  28007  pncan3s  28065  divscan2wd  28189  om2noseqoi  28295  n0sge0  28330  bdayfinbndlem1  28459  1reno  28489  axlowdimlem7  29017  axlowdimlem10  29020  axcontlem6  29038  umgrbi  29170  rusgr1vtxlem  29656  clwwlknonwwlknonb  30176  3wlkond  30241  frcond3  30339  hsn0elch  31319  axpjcl  31471  omlsilem  31473  pjchi  31503  shs00i  31521  chj00i  31558  chabs1  31587  pjspansn  31648  chscllem1  31708  osumcor2i  31715  nonbooli  31722  atcvat4i  32468  xppreima  32718  xdivrec  32986  wrdt2ind  33013  psgndmfi  33159  sqsscirc1  34052  1stmbfm  34404  2ndmbfm  34405  carsgclctunlem2  34463  eulerpartlemgh  34522  hgt750leme  34802  bnj1148  35138  bnj1154  35141  fineqvpow  35259  fineqvacALT  35261  fineqvnttrclse  35268  fineqvr1ombregs  35282  cvmlift3lem5  35505  cvmlift3lem7  35507  currybi  35870  dfon2lem3  35965  dfon2lem7  35969  distel  35983  altopthsn  36143  axtcond  36660  ttc00  36690  bj-ax12  36951  bj-exlimmpbi  37220  irrdiff  37640  rdgssun  37694  wl-ax12v2cl  37822  poimirlem9  37950  poimirlem26  37967  poimirlem27  37968  poimirlem32  37973  dvasin  38025  areacirclem4  38032  heiborlem8  38139  0rngo  38348  dfsuccl4  38795  suceldisj  39139  ax12eq  39387  ax12el  39388  ax12inda  39394  ax12v2-o  39395  nfded  39413  nfded2  39414  nfunidALT2  39415  lshpinN  39435  trlid0  40622  hdmap10lem  42285  lcmineqlem  42491  aks4d1p1p5  42514  fisdomnn  42683  asin1half  42789  renegid  42805  repncan3  42815  sn-00idlem2  42831  reixi  42855  rerecne0d  42888  sn-ltp1  42921  flt4lem7  43092  islssfg2  43499  areaquad  43644  onsupuni  43657  onov0suclim  43702  minregex  43961  wfac8prim  45429  fperdvper  46347  itgvol0  46396  stoweidlem13  46441  stoweidlem26  46454  stoweidlem34  46462  wallispilem4  46496  dirkercncflem1  46531  dirkercncflem3  46533  dirkercncflem4  46534  fourierdlem35  46570  fourierdlem73  46607  funressndmafv2rn  47671  dfatbrafv2b  47693  fnbrafv2b  47696  ichnfimlem  47923  lighneallem4b  48072  nprmdvdsfacm1lem4  48086  sbgoldbwt  48253  sbgoldbalt  48257  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  bgoldbtbndlem3  48283  grimidvtxedg  48361  tposideq  49363  iooii  49393  0thincg  49933  oduoppcciso  50041