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  1083  eqcomd  2742  eqvisset  3460  vtoclg  3511  vtocl  3515  vtoclOLD  3516  vtoclf  3521  vtoclgf  3525  vtoclg1f  3526  eueq3  3669  sbc2or  3749  csbiegf  3882  un00  4397  elimhyp  4545  elimhyp2v  4546  elimhyp3v  4547  elimhyp4v  4548  elimdhyp  4550  keephyp2v  4552  keephyp3v  4553  preq12b  4806  nfopd  4846  ssex  5266  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  6995  fvsnun2  7129  iunpw  7716  onsucuni  7770  onuninsuci  7782  tposf12  8193  oaword1  8479  oneo  8508  nnaword1  8557  nnneo  8583  naddword1  8619  1sdom2dom  9154  inficl  9328  fipwuni  9329  infeq5i  9545  cantnflt  9581  cantnflem1  9598  cnfcom  9609  brttrcl  9622  rankidn  9734  rankr1id  9774  rankxpsuc  9794  iscard  9887  iscard2  9888  carduni  9893  cardmin2  9911  infxpenlem  9923  alephgeom  9992  cardaleph  9999  infenaleph  10001  iscard3  10003  alephsson  10010  alephfp  10018  alephval3  10020  dfac12k  10058  axdc3lem2  10361  alephval2  10483  alephreg  10493  cfpwsdom  10495  alephom  10496  axrepndlem1  10503  axunndlem1  10506  axunnd  10507  axpowndlem2  10509  axpowndlem3  10510  axpowndlem4  10511  axpownd  10512  axregndlem2  10514  axinfndlem1  10516  axinfnd  10517  axacndlem4  10521  axacndlem5  10522  axacnd  10523  gchaleph2  10583  elwina  10597  elina  10598  winaon  10599  inawina  10601  winainf  10605  winalim  10606  tskr1om2  10679  r1tskina  10693  gruina  10729  grur1a  10730  indpi  10818  nqerrel  10843  recidnq  10876  ltaddnq  10885  pncan3  11388  divcan2  11804  ltp1  11981  ltm1  11983  recreclt  12041  elnn0z  12501  nn0ind-raph  12592  fzdifsuc  13500  2tnp1ge0ge0  13749  fsuppmapnn0fiubex  13915  faclbnd5  14221  hashfun  14360  ccatalpha  14517  caucvgrlem  15596  fsumcnv  15696  fprodcnv  15906  ef01bndlem  16109  sin01gt0  16115  cos01gt0  16116  egt2lt3  16131  cnso  16172  ltoddhalfle  16288  4sqlem12  16884  funcres  17820  fuchom  17888  xpsmnd  18702  xpsgrp  18989  mulgfval  18999  mulgfvalALT  19000  nmznsg  19097  frgp0  19689  gsumval3lem2  19835  gsumval3  19836  xpsrngd  20114  xpsringd  20268  pwssplit1  21011  pzriprnglem4  21439  mvrf1  21941  psdmul  22109  ply1chr  22250  blssioo  24739  dvidlem  25872  dvcj  25910  dvrec  25915  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlipcn  25955  dv11cn  25962  dvivthlem2  25970  lhop1lem  25974  lhop1  25975  lhop2  25976  q1peqb  26117  pserdv  26395  sinhalfpilem  26428  tangtx  26470  efabl  26515  logi  26552  logneg2  26580  gausslemma2dlem1a  27332  lgseisenlem4  27345  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  dchrisum0lem3  27486  mulogsum  27499  pntrlog2bndlem1  27544  madebday  27896  ltsp1d  28011  pncan3s  28069  divscan2wd  28193  om2noseqoi  28299  n0sge0  28334  bdayfinbndlem1  28463  1reno  28493  axlowdimlem7  29021  axlowdimlem10  29024  axcontlem6  29042  umgrbi  29174  rusgr1vtxlem  29661  clwwlknonwwlknonb  30181  3wlkond  30246  frcond3  30344  hsn0elch  31323  axpjcl  31475  omlsilem  31477  pjchi  31507  shs00i  31525  chj00i  31562  chabs1  31591  pjspansn  31652  chscllem1  31712  osumcor2i  31719  nonbooli  31726  atcvat4i  32472  xppreima  32723  xdivrec  33008  wrdt2ind  33035  psgndmfi  33180  sqsscirc1  34065  1stmbfm  34417  2ndmbfm  34418  carsgclctunlem2  34476  eulerpartlemgh  34535  hgt750leme  34815  bnj1148  35152  bnj1154  35155  fineqvpow  35271  fineqvacALT  35273  fineqvnttrclse  35280  fineqvr1ombregs  35294  cvmlift3lem5  35517  cvmlift3lem7  35519  currybi  35882  dfon2lem3  35977  dfon2lem7  35981  distel  35995  altopthsn  36155  bj-ax12  36858  bj-exlimmpbi  37114  irrdiff  37527  rdgssun  37579  wl-ax12v2cl  37707  poimirlem9  37826  poimirlem26  37843  poimirlem27  37844  poimirlem32  37849  dvasin  37901  areacirclem4  37908  heiborlem8  38015  0rngo  38224  dfsuccl4  38644  ax12eq  39197  ax12el  39198  ax12inda  39204  ax12v2-o  39205  nfded  39223  nfded2  39224  nfunidALT2  39225  lshpinN  39245  trlid0  40432  hdmap10lem  42095  lcmineqlem  42302  aks4d1p1p5  42325  fisdomnn  42495  asin1half  42608  renegid  42624  repncan3  42634  sn-00idlem2  42650  reixi  42674  sn-ltp1  42727  flt4lem7  42898  islssfg2  43309  areaquad  43454  onsupuni  43467  onov0suclim  43512  minregex  43771  wfac8prim  45239  fperdvper  46159  itgvol0  46208  stoweidlem13  46253  stoweidlem26  46266  stoweidlem34  46274  wallispilem4  46308  dirkercncflem1  46343  dirkercncflem3  46345  dirkercncflem4  46346  fourierdlem35  46382  fourierdlem73  46419  funressndmafv2rn  47465  dfatbrafv2b  47487  fnbrafv2b  47490  ichnfimlem  47705  lighneallem4b  47851  sbgoldbwt  48019  sbgoldbalt  48023  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  bgoldbtbndlem1  48047  bgoldbtbndlem3  48049  grimidvtxedg  48127  tposideq  49129  iooii  49159  0thincg  49699  oduoppcciso  49807