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  2737  eqvisset  3456  vtoclg  3509  vtocl  3513  vtoclOLD  3514  vtoclf  3519  vtoclgf  3524  vtoclg1f  3525  vtoclgOLD  3526  eueq3  3670  sbc2or  3750  csbiegf  3883  un00  4395  elimhyp  4541  elimhyp2v  4542  elimhyp3v  4543  elimhyp4v  4544  elimdhyp  4546  keephyp2v  4548  keephyp3v  4549  preq12b  4802  nfopd  4842  ssex  5259  opthwiener  5454  isso2i  5561  nfimad  6018  dfrel2  6136  ordtri3or  6338  on0eqel  6431  funsng  6532  cnvresid  6560  nffvd  6834  fnbrfvb  6872  fvelrnb  6882  fvelimab  6894  funfvop  6983  fvsnun2  7117  iunpw  7704  onsucuni  7758  onuninsuci  7770  tposf12  8181  oaword1  8467  oneo  8496  nnaword1  8544  nnneo  8570  naddword1  8606  1sdom2dom  9138  inficl  9309  fipwuni  9310  infeq5i  9526  cantnflt  9562  cantnflem1  9579  cnfcom  9590  brttrcl  9603  rankidn  9712  rankr1id  9752  rankxpsuc  9772  iscard  9865  iscard2  9866  carduni  9871  cardmin2  9889  infxpenlem  9901  alephgeom  9970  cardaleph  9977  infenaleph  9979  iscard3  9981  alephsson  9988  alephfp  9996  alephval3  9998  dfac12k  10036  axdc3lem2  10339  alephval2  10460  alephreg  10470  cfpwsdom  10472  alephom  10473  axrepndlem1  10480  axunndlem1  10483  axunnd  10484  axpowndlem2  10486  axpowndlem3  10487  axpowndlem4  10488  axpownd  10489  axregndlem2  10491  axinfndlem1  10493  axinfnd  10494  axacndlem4  10498  axacndlem5  10499  axacnd  10500  gchaleph2  10560  elwina  10574  elina  10575  winaon  10576  inawina  10578  winainf  10582  winalim  10583  tskr1om2  10656  r1tskina  10670  gruina  10706  grur1a  10707  indpi  10795  nqerrel  10820  recidnq  10853  ltaddnq  10862  pncan3  11365  divcan2  11781  ltp1  11958  ltm1  11960  recreclt  12018  elnn0z  12478  nn0ind-raph  12570  fzdifsuc  13481  2tnp1ge0ge0  13730  fsuppmapnn0fiubex  13896  faclbnd5  14202  hashfun  14341  ccatalpha  14498  caucvgrlem  15577  fsumcnv  15677  fprodcnv  15887  ef01bndlem  16090  sin01gt0  16096  cos01gt0  16097  egt2lt3  16112  cnso  16153  ltoddhalfle  16269  4sqlem12  16865  funcres  17800  fuchom  17868  xpsmnd  18682  xpsgrp  18969  mulgfval  18979  mulgfvalALT  18980  nmznsg  19078  frgp0  19670  gsumval3lem2  19816  gsumval3  19817  xpsrngd  20095  xpsringd  20248  pwssplit1  20991  pzriprnglem4  21419  mvrf1  21921  psdmul  22079  ply1chr  22219  blssioo  24708  dvidlem  25841  dvcj  25879  dvrec  25884  rolle  25919  cmvth  25920  cmvthOLD  25921  mvth  25922  dvlip  25923  dvlipcn  25924  dv11cn  25931  dvivthlem2  25939  lhop1lem  25943  lhop1  25944  lhop2  25945  q1peqb  26086  pserdv  26364  sinhalfpilem  26397  tangtx  26439  efabl  26484  logi  26521  logneg2  26549  gausslemma2dlem1a  27301  lgseisenlem4  27314  2lgslem3a  27332  2lgslem3b  27333  2lgslem3c  27334  2lgslem3d  27335  dchrisum0lem3  27455  mulogsum  27468  pntrlog2bndlem1  27513  madebday  27843  sltp1d  27956  pncan3s  28011  divscan2wd  28134  om2noseqoi  28231  n0sge0  28264  axlowdimlem7  28924  axlowdimlem10  28927  axcontlem6  28945  umgrbi  29077  rusgr1vtxlem  29564  clwwlknonwwlknonb  30081  3wlkond  30146  frcond3  30244  hsn0elch  31223  axpjcl  31375  omlsilem  31377  pjchi  31407  shs00i  31425  chj00i  31462  chabs1  31491  pjspansn  31552  chscllem1  31612  osumcor2i  31619  nonbooli  31626  atcvat4i  32372  xppreima  32622  xdivrec  32902  wrdt2ind  32929  psgndmfi  33062  sqsscirc1  33916  1stmbfm  34268  2ndmbfm  34269  carsgclctunlem2  34327  eulerpartlemgh  34386  hgt750leme  34666  bnj1148  35003  bnj1154  35006  fineqvr1ombregs  35123  fineqvpow  35126  fineqvacALT  35128  fineqvnttrclse  35132  cvmlift3lem5  35355  cvmlift3lem7  35357  currybi  35720  dfon2lem3  35818  dfon2lem7  35822  distel  35836  altopthsn  35994  bj-ax12  36690  bj-exlimmpbi  36946  irrdiff  37359  rdgssun  37411  wl-ax12v2cl  37539  poimirlem9  37668  poimirlem26  37685  poimirlem27  37686  poimirlem32  37691  dvasin  37743  areacirclem4  37750  heiborlem8  37857  0rngo  38066  ax12eq  38979  ax12el  38980  ax12inda  38986  ax12v2-o  38987  nfded  39005  nfded2  39006  nfunidALT2  39007  lshpinN  39027  trlid0  40214  hdmap10lem  41877  lcmineqlem  42084  aks4d1p1p5  42107  fisdomnn  42276  asin1half  42389  renegid  42405  repncan3  42415  sn-00idlem2  42431  reixi  42455  sn-ltp1  42508  flt4lem7  42691  islssfg2  43103  areaquad  43248  onsupuni  43261  onov0suclim  43306  minregex  43566  wfac8prim  45034  fperdvper  45956  itgvol0  46005  stoweidlem13  46050  stoweidlem26  46063  stoweidlem34  46071  wallispilem4  46105  dirkercncflem1  46140  dirkercncflem3  46142  dirkercncflem4  46143  fourierdlem35  46179  fourierdlem73  46216  funressndmafv2rn  47253  dfatbrafv2b  47275  fnbrafv2b  47278  ichnfimlem  47493  lighneallem4b  47639  sbgoldbwt  47807  sbgoldbalt  47811  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  bgoldbtbndlem1  47835  bgoldbtbndlem3  47837  grimidvtxedg  47915  tposideq  48918  iooii  48948  0thincg  49489  oduoppcciso  49597