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  3462  vtoclg  3513  vtocl  3517  vtoclOLD  3518  vtoclf  3523  vtoclgf  3527  vtoclg1f  3528  eueq3  3671  sbc2or  3751  csbiegf  3884  un00  4399  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  preq12b  4808  nfopd  4848  ssex  5268  opthwiener  5470  isso2i  5577  nfimad  6036  dfrel2  6155  ordtri3or  6357  on0eqel  6450  funsng  6551  cnvresid  6579  nffvd  6854  fnbrfvb  6892  fvelrnb  6902  fvelimab  6914  funfvop  7004  fvsnun2  7139  iunpw  7726  onsucuni  7780  onuninsuci  7792  tposf12  8203  oaword1  8489  oneo  8518  nnaword1  8567  nnneo  8593  naddword1  8629  1sdom2dom  9166  inficl  9340  fipwuni  9341  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  11400  divcan2  11816  ltp1  11993  ltm1  11995  recreclt  12053  elnn0z  12513  nn0ind-raph  12604  fzdifsuc  13512  2tnp1ge0ge0  13761  fsuppmapnn0fiubex  13927  faclbnd5  14233  hashfun  14372  ccatalpha  14529  caucvgrlem  15608  fsumcnv  15708  fprodcnv  15918  ef01bndlem  16121  sin01gt0  16127  cos01gt0  16128  egt2lt3  16143  cnso  16184  ltoddhalfle  16300  4sqlem12  16896  funcres  17832  fuchom  17900  xpsmnd  18714  xpsgrp  19001  mulgfval  19011  mulgfvalALT  19012  nmznsg  19109  frgp0  19701  gsumval3lem2  19847  gsumval3  19848  xpsrngd  20126  xpsringd  20280  pwssplit1  21023  pzriprnglem4  21451  mvrf1  21953  psdmul  22121  ply1chr  22262  blssioo  24751  dvidlem  25884  dvcj  25922  dvrec  25927  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlipcn  25967  dv11cn  25974  dvivthlem2  25982  lhop1lem  25986  lhop1  25987  lhop2  25988  q1peqb  26129  pserdv  26407  sinhalfpilem  26440  tangtx  26482  efabl  26527  logi  26564  logneg2  26592  gausslemma2dlem1a  27344  lgseisenlem4  27357  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  dchrisum0lem3  27498  mulogsum  27511  pntrlog2bndlem1  27556  madebday  27908  ltsp1d  28023  pncan3s  28081  divscan2wd  28205  om2noseqoi  28311  n0sge0  28346  bdayfinbndlem1  28475  1reno  28505  axlowdimlem7  29033  axlowdimlem10  29036  axcontlem6  29054  umgrbi  29186  rusgr1vtxlem  29673  clwwlknonwwlknonb  30193  3wlkond  30258  frcond3  30356  hsn0elch  31335  axpjcl  31487  omlsilem  31489  pjchi  31519  shs00i  31537  chj00i  31574  chabs1  31603  pjspansn  31664  chscllem1  31724  osumcor2i  31731  nonbooli  31738  atcvat4i  32484  xppreima  32734  xdivrec  33018  wrdt2ind  33045  psgndmfi  33191  sqsscirc1  34085  1stmbfm  34437  2ndmbfm  34438  carsgclctunlem2  34496  eulerpartlemgh  34555  hgt750leme  34835  bnj1148  35171  bnj1154  35174  fineqvpow  35290  fineqvacALT  35292  fineqvnttrclse  35299  fineqvr1ombregs  35313  cvmlift3lem5  35536  cvmlift3lem7  35538  currybi  35901  dfon2lem3  35996  dfon2lem7  36000  distel  36014  altopthsn  36174  bj-ax12  36896  bj-exlimmpbi  37155  irrdiff  37575  rdgssun  37627  wl-ax12v2cl  37755  poimirlem9  37874  poimirlem26  37891  poimirlem27  37892  poimirlem32  37897  dvasin  37949  areacirclem4  37956  heiborlem8  38063  0rngo  38272  dfsuccl4  38719  suceldisj  39063  ax12eq  39311  ax12el  39312  ax12inda  39318  ax12v2-o  39319  nfded  39337  nfded2  39338  nfunidALT2  39339  lshpinN  39359  trlid0  40546  hdmap10lem  42209  lcmineqlem  42416  aks4d1p1p5  42439  fisdomnn  42608  asin1half  42721  renegid  42737  repncan3  42747  sn-00idlem2  42763  reixi  42787  sn-ltp1  42840  flt4lem7  43011  islssfg2  43422  areaquad  43567  onsupuni  43580  onov0suclim  43625  minregex  43884  wfac8prim  45352  fperdvper  46271  itgvol0  46320  stoweidlem13  46365  stoweidlem26  46378  stoweidlem34  46386  wallispilem4  46420  dirkercncflem1  46455  dirkercncflem3  46457  dirkercncflem4  46458  fourierdlem35  46494  fourierdlem73  46531  funressndmafv2rn  47577  dfatbrafv2b  47599  fnbrafv2b  47602  ichnfimlem  47817  lighneallem4b  47963  sbgoldbwt  48131  sbgoldbalt  48135  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  bgoldbtbndlem1  48159  bgoldbtbndlem3  48161  grimidvtxedg  48239  tposideq  49241  iooii  49271  0thincg  49811  oduoppcciso  49919