Theorem mpbii 224

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  elimh  1096  axc15  2470  eqcomd  2808  eqvisset  3401  vtoclgf  3453  vtoclg1f  3454  eueq3  3573  sbc2or  3636  csbiegf  3746  un00  4203  elimhyp  4336  elimhyp2v  4337  elimhyp3v  4338  elimhyp4v  4339  elimdhyp  4341  keephyp2v  4343  keephyp3v  4344  preq12b  4562  prel12OLD  4563  nfopd  4605  ssex  4991  opthwiener  5163  isso2i  5258  nfimad  5679  dfrel2  5788  ordtri3or  5962  on0eqel  6052  funsng  6145  cnvresid  6173  nffvd  6414  fnbrfvb  6450  fvelrnb  6458  fvelimab  6468  funfvop  6545  iunpw  7202  onsucuni  7252  onuninsuci  7264  tposf12  7606  oaword1  7863  oneo  7892  nnaword1  7940  nnneo  7962  inficl  8564  fipwuni  8565  infeq5i  8774  cantnflt  8810  cantnflem1  8827  cnfcom  8838  rankidn  8926  rankr1id  8966  rankxpsuc  8986  iscard  9078  iscard2  9079  carduni  9084  cardmin2  9101  infxpenlem  9113  alephgeom  9182  cardaleph  9189  infenaleph  9191  iscard3  9193  alephsson  9200  alephfp  9208  alephval3  9210  dfac12k  9248  axdc3lem2  9552  alephval2  9673  alephreg  9683  cfpwsdom  9685  alephom  9686  axrepndlem1  9693  axunndlem1  9696  axunnd  9697  axpowndlem2  9699  axpowndlem3  9700  axpowndlem4  9701  axpownd  9702  axregndlem2  9704  axinfndlem1  9706  axinfnd  9707  axacndlem4  9711  axacndlem5  9712  axacnd  9713  gchaleph2  9773  elwina  9787  elina  9788  winaon  9789  inawina  9791  winainf  9795  winalim  9796  tskr1om2  9869  r1tskina  9883  gruina  9919  grur1a  9920  indpi  10008  nqerrel  10033  recidnq  10066  ltaddnq  10075  pncan3  10568  divcan2  10972  ltp1  11140  ltm1  11142  recreclt  11201  elnn0z  11650  nn0ind-raph  11737  fzdifsuc  12617  2tnp1ge0ge0  12848  fsuppmapnn0fiubex  13009  faclbnd5  13299  hashfun  13435  ccatalpha  13584  caucvgrlem  14620  fsumcnv  14721  fprodcnv  14928  ef01bndlem  15128  sin01gt0  15134  cos01gt0  15135  egt2lt3  15148  cnso  15190  ltoddhalfle  15299  4sqlem12  15871  funcres  16754  fuchom  16819  xpsmnd  17529  xpsgrp  17733  mulgfval  17741  nmznsg  17834  symgplusg  18004  frgp0  18368  gsumval3lem1  18501  gsumval3lem2  18502  gsumval3  18503  pwssplit1  19260  mvrf1  19628  blssioo  22805  dvidlem  23887  dvcj  23921  dvrec  23926  rolle  23961  cmvth  23962  mvth  23963  dvlip  23964  dvlipcn  23965  dv11cn  23972  dvivthlem2  23980  lhop1lem  23984  lhop1  23985  lhop2  23986  q1peqb  24122  pserdv  24391  sinhalfpilem  24424  tangtx  24466  efabl  24505  logneg2  24569  gausslemma2dlem1a  25298  lgseisenlem4  25311  2lgslem3a  25329  2lgslem3b  25330  2lgslem3c  25331  2lgslem3d  25332  dchrisum0lem3  25416  mulogsum  25429  pntrlog2bndlem1  25474  axlowdimlem7  26036  axlowdimlem10  26039  axcontlem6  26057  umgrbi  26204  rusgr1vtxlem  26705  3wlkond  27338  frcond3  27438  hsn0elch  28427  axpjcl  28581  omlsilem  28583  pjchi  28613  shs00i  28631  chj00i  28668  chabs1  28697  pjspansn  28758  chscllem1  28818  osumcor2i  28825  nonbooli  28832  atcvat4i  29578  xppreima  29770  xdivrec  29954  psgndmfi  30165  sqsscirc1  30273  1stmbfm  30641  2ndmbfm  30642  carsgclctunlem2  30700  eulerpartlemgh  30759  hgt750leme  31055  bnj1148  31381  bnj1154  31384  cvmlift3lem5  31622  cvmlift3lem7  31624  logi  31936  dfon2lem3  32004  dfon2lem7  32008  distel  32023  altopthsn  32383  bj-exlimmpbi  33209  poimirlem9  33725  poimirlem26  33742  poimirlem27  33743  poimirlem32  33748  dvasin  33802  areacirclem4  33809  heiborlem8  33922  0rngo  34131  ax12eq  34714  ax12el  34715  ax12inda  34721  ax12v2-o  34722  nfded  34741  nfded2  34742  nfunidALT2  34743  lshpinN  34763  trlid0  35951  hdmap10lem  37614  islssfg2  38136  areaquad  38296  rnmptc  39836  fperdvper  40607  itgvol0  40657  stoweidlem13  40703  stoweidlem26  40716  stoweidlem34  40724  wallispilem4  40758  dirkercncflem1  40793  dirkercncflem3  40795  dirkercncflem4  40796  fourierdlem35  40832  fourierdlem73  40869  funressndmafv2rn  41806  dfatbrafv2b  41828  fnbrafv2b  41831  lighneallem4b  42095  sbgoldbwt  42234  sbgoldbalt  42238  nnsum4primeseven  42257  nnsum4primesevenALTV  42258  bgoldbtbndlem1  42262  bgoldbtbndlem3  42264