Theorem mpbii 235

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 234	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  dedt  1094  eqcomd  2767  eqvisset  3473  vtoclg  3521  vtocl  3524  vtoclOLD  3525  vtoclf  3530  vtoclgf  3534  vtoclg1f  3535  eueq3  3673  sbc2or  3753  csbiegf  3885  un00  4398  elimhyp  4545  elimhyp2v  4546  elimhyp3v  4547  elimhyp4v  4548  elimdhyp  4550  keephyp2v  4552  keephyp3v  4553  preq12b  4807  nfopd  4847  ssex  5276  opthwiener  5482  isso2i  5590  nfimad  6055  dfrel2  6171  ordtri3or  6374  on0eqel  6467  funsng  6568  cnvresid  6596  nffvd  6875  fnbrfvb  6913  fvelrnb  6923  fvelimab  6935  funfvop  7027  fvsnun2  7163  iunpw  7750  onsucuni  7804  onuninsuci  7816  tposf12  8226  oaword1  8516  oneo  8545  nnaword1  8594  nnneo  8620  naddword1  8657  1sdom2dom  9194  inficl  9368  fipwuni  9369  infeq5i  9588  cantnflt  9624  cantnflem1  9641  cnfcom  9652  brttrcl  9665  rankidn  9777  rankr1id  9817  rankxpsuc  9837  iscard  9930  iscard2  9931  carduni  9936  cardmin2  9954  infxpenlem  9966  alephgeom  10035  cardaleph  10042  infenaleph  10044  iscard3  10046  alephsson  10053  alephfp  10061  alephval3  10063  dfac12k  10101  axdc3lem2  10405  alephval2  10527  alephreg  10537  cfpwsdom  10539  alephom  10540  axrepndlem1  10547  axunndlem1  10550  axunnd  10551  axpowndlem2  10553  axpowndlem3  10554  axpowndlem4  10555  axpownd  10556  axregndlem2  10558  axinfndlem1  10560  axinfnd  10561  axacndlem4  10565  axacndlem5  10566  axacnd  10567  gchaleph2  10627  elwina  10641  elina  10642  winaon  10643  inawina  10645  winainf  10649  winalim  10650  tskr1om2  10723  r1tskina  10737  gruina  10773  grur1a  10774  indpi  10862  nqerrel  10887  recidnq  10920  ltaddnq  10929  pncan3  11435  divcan2  11850  ltp1  12028  ltm1  12030  recreclt  12088  elnn0z  12578  nn0ind-raph  12670  fzdifsuc  13586  2tnp1ge0ge0  13836  fsuppmapnn0fiubex  14002  faclbnd5  14308  hashfun  14447  ccatalpha  14604  caucvgrlem  15683  fsumcnv  15783  fprodcnv  15996  ef01bndlem  16199  sin01gt0  16205  cos01gt0  16206  egt2lt3  16221  cnso  16262  ltoddhalfle  16378  4sqlem12  16975  funcres  17912  fuchom  17980  xpsmnd  18794  xpsgrp  19084  mulgfval  19094  mulgfvalALT  19095  nmznsg  19192  frgp0  19783  gsumval3lem2  19929  gsumval3  19930  xpsrngd  20208  xpsringd  20360  pwssplit1  21106  pzriprnglem4  21516  mvrf1  22017  psdmul  22211  ply1chr  22349  blssioo  24835  dvidlem  25957  dvcj  25992  dvrec  25997  rolle  26032  cmvth  26033  mvth  26034  dvlip  26035  dvlipcn  26036  dv11cn  26043  dvivthlem2  26051  lhop1lem  26055  lhop1  26056  lhop2  26057  q1peqb  26196  pserdv  26469  sinhalfpilem  26505  tangtx  26547  efabl  26592  logi  26629  logneg2  26657  gausslemma2dlem1a  27406  lgseisenlem4  27419  2lgslem3a  27437  2lgslem3b  27438  2lgslem3c  27439  2lgslem3d  27440  dchrisum0lem3  27560  mulogsum  27573  pntrlog2bndlem1  27618  madebday  27970  ltsp1d  28085  pncan3s  28143  divscan2wd  28267  om2noseqoi  28373  n0sge0  28408  bdayfinbndlem1  28537  1reno  28567  axlowdimlem7  29095  axlowdimlem10  29098  axcontlem6  29116  umgrbi  29248  rusgr1vtxlem  29734  clwwlknonwwlknonb  30254  3wlkond  30319  frcond3  30417  hsn0elch  31397  axpjcl  31549  omlsilem  31551  pjchi  31581  shs00i  31599  chj00i  31636  chabs1  31665  pjspansn  31726  chscllem1  31786  osumcor2i  31793  nonbooli  31800  atcvat4i  32546  xppreima  32797  xdivrec  33065  wrdt2ind  33092  psgndmfi  33239  sqsscirc1  34166  1stmbfm  34518  2ndmbfm  34519  carsgclctunlem2  34577  eulerpartlemgh  34636  hgt750leme  34916  bnj1148  35255  bnj1154  35258  fineqvpow  35375  fineqvacALT  35377  fineqvnttrclse  35384  fineqvr1ombregs  35398  cvmlift3lem5  35637  cvmlift3lem7  35639  currybi  36002  dfon2lem3  36097  dfon2lem7  36101  distel  36115  altopthsn  36275  axtcond  36802  ttc00  36832  bj-ax12  37093  bj-exlimmpbi  37362  irrdiff  37782  rdgssun  37836  wl-ax12v2cl  37964  poimirlem9  38092  poimirlem26  38109  poimirlem27  38110  poimirlem32  38115  dvasin  38167  areacirclem4  38174  heiborlem8  38281  0rngo  38490  dfsuccl4  38937  suceldisj  39281  ax12eq  39529  ax12el  39530  ax12inda  39536  ax12v2-o  39537  nfded  39555  nfded2  39556  nfunidALT2  39557  lshpinN  39577  trlid0  40764  hdmap10lem  42427  lcmineqlem  42633  aks4d1p1p5  42656  fisdomnn  42824  asin1half  42930  renegid  42946  repncan3  42956  sn-00idlem2  42972  reixi  42996  rerecne0d  43029  sn-ltp1  43062  flt4lem7  43205  islssfg2  43612  areaquad  43757  onsupuni  43770  onov0suclim  43815  minregex  44074  wfac8prim  45542  fperdvper  46457  itgvol0  46506  stoweidlem13  46551  stoweidlem26  46564  stoweidlem34  46572  wallispilem4  46606  dirkercncflem1  46641  dirkercncflem3  46643  dirkercncflem4  46644  fourierdlem35  46680  fourierdlem73  46717  funressndmafv2rn  47781  dfatbrafv2b  47803  fnbrafv2b  47806  ichnfimlem  48033  lighneallem4b  48182  nprmdvdsfacm1lem4  48196  sbgoldbwt  48363  sbgoldbalt  48367  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  bgoldbtbndlem1  48391  bgoldbtbndlem3  48393  grimidvtxedg  48471  tposideq  49473  iooii  49503  0thincg  50043  oduoppcciso  50151