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  2743  eqvisset  3450  vtoclg  3500  vtocl  3504  vtoclOLD  3505  vtoclf  3510  vtoclgf  3514  vtoclg1f  3515  eueq3  3658  sbc2or  3738  csbiegf  3871  un00  4386  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elimdhyp  4538  keephyp2v  4540  keephyp3v  4541  preq12b  4794  nfopd  4834  ssex  5258  opthwiener  5462  isso2i  5569  nfimad  6028  dfrel2  6147  ordtri3or  6349  on0eqel  6442  funsng  6543  cnvresid  6571  nffvd  6846  fnbrfvb  6884  fvelrnb  6894  fvelimab  6906  funfvop  6996  fvsnun2  7131  iunpw  7718  onsucuni  7772  onuninsuci  7784  tposf12  8194  oaword1  8480  oneo  8509  nnaword1  8558  nnneo  8584  naddword1  8620  1sdom2dom  9157  inficl  9331  fipwuni  9332  infeq5i  9548  cantnflt  9584  cantnflem1  9601  cnfcom  9612  brttrcl  9625  rankidn  9737  rankr1id  9777  rankxpsuc  9797  iscard  9890  iscard2  9891  carduni  9896  cardmin2  9914  infxpenlem  9926  alephgeom  9995  cardaleph  10002  infenaleph  10004  iscard3  10006  alephsson  10013  alephfp  10021  alephval3  10023  dfac12k  10061  axdc3lem2  10364  alephval2  10486  alephreg  10496  cfpwsdom  10498  alephom  10499  axrepndlem1  10506  axunndlem1  10509  axunnd  10510  axpowndlem2  10512  axpowndlem3  10513  axpowndlem4  10514  axpownd  10515  axregndlem2  10517  axinfndlem1  10519  axinfnd  10520  axacndlem4  10524  axacndlem5  10525  axacnd  10526  gchaleph2  10586  elwina  10600  elina  10601  winaon  10602  inawina  10604  winainf  10608  winalim  10609  tskr1om2  10682  r1tskina  10696  gruina  10732  grur1a  10733  indpi  10821  nqerrel  10846  recidnq  10879  ltaddnq  10888  pncan3  11392  divcan2  11808  ltp1  11986  ltm1  11988  recreclt  12046  elnn0z  12528  nn0ind-raph  12620  fzdifsuc  13529  2tnp1ge0ge0  13779  fsuppmapnn0fiubex  13945  faclbnd5  14251  hashfun  14390  ccatalpha  14547  caucvgrlem  15626  fsumcnv  15726  fprodcnv  15939  ef01bndlem  16142  sin01gt0  16148  cos01gt0  16149  egt2lt3  16164  cnso  16205  ltoddhalfle  16321  4sqlem12  16918  funcres  17854  fuchom  17922  xpsmnd  18736  xpsgrp  19026  mulgfval  19036  mulgfvalALT  19037  nmznsg  19134  frgp0  19726  gsumval3lem2  19872  gsumval3  19873  xpsrngd  20151  xpsringd  20303  pwssplit1  21046  pzriprnglem4  21474  mvrf1  21974  psdmul  22142  ply1chr  22281  blssioo  24770  dvidlem  25892  dvcj  25927  dvrec  25932  rolle  25967  cmvth  25968  mvth  25969  dvlip  25970  dvlipcn  25971  dv11cn  25978  dvivthlem2  25986  lhop1lem  25990  lhop1  25991  lhop2  25992  q1peqb  26131  pserdv  26407  sinhalfpilem  26440  tangtx  26482  efabl  26527  logi  26564  logneg2  26592  gausslemma2dlem1a  27342  lgseisenlem4  27355  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  dchrisum0lem3  27496  mulogsum  27509  pntrlog2bndlem1  27554  madebday  27906  ltsp1d  28021  pncan3s  28079  divscan2wd  28203  om2noseqoi  28309  n0sge0  28344  bdayfinbndlem1  28473  1reno  28503  axlowdimlem7  29031  axlowdimlem10  29034  axcontlem6  29052  umgrbi  29184  rusgr1vtxlem  29671  clwwlknonwwlknonb  30191  3wlkond  30256  frcond3  30354  hsn0elch  31334  axpjcl  31486  omlsilem  31488  pjchi  31518  shs00i  31536  chj00i  31573  chabs1  31602  pjspansn  31663  chscllem1  31723  osumcor2i  31730  nonbooli  31737  atcvat4i  32483  xppreima  32733  xdivrec  33001  wrdt2ind  33028  psgndmfi  33174  sqsscirc1  34068  1stmbfm  34420  2ndmbfm  34421  carsgclctunlem2  34479  eulerpartlemgh  34538  hgt750leme  34818  bnj1148  35154  bnj1154  35157  fineqvpow  35275  fineqvacALT  35277  fineqvnttrclse  35284  fineqvr1ombregs  35298  cvmlift3lem5  35521  cvmlift3lem7  35523  currybi  35886  dfon2lem3  35981  dfon2lem7  35985  distel  35999  altopthsn  36159  axtcond  36676  ttc00  36706  bj-ax12  36967  bj-exlimmpbi  37236  irrdiff  37656  rdgssun  37708  wl-ax12v2cl  37836  poimirlem9  37964  poimirlem26  37981  poimirlem27  37982  poimirlem32  37987  dvasin  38039  areacirclem4  38046  heiborlem8  38153  0rngo  38362  dfsuccl4  38809  suceldisj  39153  ax12eq  39401  ax12el  39402  ax12inda  39408  ax12v2-o  39409  nfded  39427  nfded2  39428  nfunidALT2  39429  lshpinN  39449  trlid0  40636  hdmap10lem  42299  lcmineqlem  42505  aks4d1p1p5  42528  fisdomnn  42697  asin1half  42803  renegid  42819  repncan3  42829  sn-00idlem2  42845  reixi  42869  rerecne0d  42902  sn-ltp1  42935  flt4lem7  43106  islssfg2  43517  areaquad  43662  onsupuni  43675  onov0suclim  43720  minregex  43979  wfac8prim  45447  fperdvper  46365  itgvol0  46414  stoweidlem13  46459  stoweidlem26  46472  stoweidlem34  46480  wallispilem4  46514  dirkercncflem1  46549  dirkercncflem3  46551  dirkercncflem4  46552  fourierdlem35  46588  fourierdlem73  46625  funressndmafv2rn  47683  dfatbrafv2b  47705  fnbrafv2b  47708  ichnfimlem  47935  lighneallem4b  48084  nprmdvdsfacm1lem4  48098  sbgoldbwt  48265  sbgoldbalt  48269  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbtbndlem1  48293  bgoldbtbndlem3  48295  grimidvtxedg  48373  tposideq  49375  iooii  49405  0thincg  49945  oduoppcciso  50053