Theorem mpbii 225

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  elimhOLD  1063  dedt  1064  axc15OLD  2359  eqcomd  2779  eqvisset  3427  vtoclgf  3479  vtoclg1f  3480  eueq3  3611  sbc2or  3685  csbiegf  3807  un00  4272  elimhyp  4408  elimhyp2v  4409  elimhyp3v  4410  elimhyp4v  4411  elimdhyp  4413  keephyp2v  4415  keephyp3v  4416  preq12b  4652  nfopd  4691  ssex  5078  opthwiener  5257  isso2i  5357  nfimad  5777  dfrel2  5884  ordtri3or  6059  on0eqel  6144  funsng  6236  cnvresid  6264  nffvd  6509  fnbrfvb  6546  fvelrnb  6554  fvelimab  6565  funfvop  6644  fvsnun2  6769  rnmptc  6795  iunpw  7308  onsucuni  7358  onuninsuci  7370  tposf12  7719  oaword1  7978  oneo  8007  nnaword1  8055  nnneo  8077  inficl  8683  fipwuni  8684  infeq5i  8892  cantnflt  8928  cantnflem1  8945  cnfcom  8956  rankidn  9044  rankr1id  9084  rankxpsuc  9104  iscard  9197  iscard2  9198  carduni  9203  cardmin2  9220  infxpenlem  9232  alephgeom  9301  cardaleph  9308  infenaleph  9310  iscard3  9312  alephsson  9319  alephfp  9327  alephval3  9329  dfac12k  9366  axdc3lem2  9670  alephval2  9791  alephreg  9801  cfpwsdom  9803  alephom  9804  axrepndlem1  9811  axunndlem1  9814  axunnd  9815  axpowndlem2  9817  axpowndlem3  9818  axpowndlem4  9819  axpownd  9820  axregndlem2  9822  axinfndlem1  9824  axinfnd  9825  axacndlem4  9829  axacndlem5  9830  axacnd  9831  gchaleph2  9891  elwina  9905  elina  9906  winaon  9907  inawina  9909  winainf  9913  winalim  9914  tskr1om2  9987  r1tskina  10001  gruina  10037  grur1a  10038  indpi  10126  nqerrel  10151  recidnq  10184  ltaddnq  10193  pncan3  10693  pncan3OLD  10694  divcan2  11106  ltp1  11280  ltm1  11282  recreclt  11339  elnn0z  11805  nn0ind-raph  11894  fzdifsuc  12782  2tnp1ge0ge0  13013  fsuppmapnn0fiubex  13174  faclbnd5  13472  hashfun  13610  ccatalpha  13755  caucvgrlem  14889  fsumcnv  14987  fprodcnv  15196  ef01bndlem  15396  sin01gt0  15402  cos01gt0  15403  egt2lt3  15418  cnso  15459  ltoddhalfle  15569  4sqlem12  16147  funcres  17037  fuchom  17102  xpsmnd  17811  xpsgrp  18018  mulgfval  18026  mulgfvalALT  18027  nmznsg  18120  symgplusg  18291  frgp0  18659  gsumval3lem2  18793  gsumval3  18794  pwssplit1  19566  mvrf1  19932  blssioo  23122  dvidlem  24232  dvcj  24266  dvrec  24271  rolle  24306  cmvth  24307  mvth  24308  dvlip  24309  dvlipcn  24310  dv11cn  24317  dvivthlem2  24325  lhop1lem  24329  lhop1  24330  lhop2  24331  q1peqb  24467  pserdv  24736  sinhalfpilem  24768  tangtx  24810  efabl  24851  logneg2  24915  gausslemma2dlem1a  25659  lgseisenlem4  25672  2lgslem3a  25690  2lgslem3b  25691  2lgslem3c  25692  2lgslem3d  25693  dchrisum0lem3  25813  mulogsum  25826  pntrlog2bndlem1  25871  axlowdimlem7  26453  axlowdimlem10  26456  axcontlem6  26474  umgrbi  26605  rusgr1vtxlem  27088  3wlkond  27716  frcond3  27819  hsn0elch  28820  axpjcl  28974  omlsilem  28976  pjchi  29006  shs00i  29024  chj00i  29061  chabs1  29090  pjspansn  29151  chscllem1  29211  osumcor2i  29218  nonbooli  29225  atcvat4i  29971  xppreima  30174  xdivrec  30374  wrdt2ind  30393  psgndmfi  30721  sqsscirc1  30828  1stmbfm  31196  2ndmbfm  31197  carsgclctunlem2  31255  eulerpartlemgh  31314  hgt750leme  31610  bnj1148  31946  bnj1154  31949  cvmlift3lem5  32188  cvmlift3lem7  32190  logi  32519  dfon2lem3  32583  dfon2lem7  32587  distel  32602  altopthsn  32976  bj-ax12  33531  bj-exlimmpbi  33754  rdgssun  34134  poimirlem9  34375  poimirlem26  34392  poimirlem27  34393  poimirlem32  34398  dvasin  34452  areacirclem4  34459  heiborlem8  34571  0rngo  34780  ax12eq  35555  ax12el  35556  ax12inda  35562  ax12v2-o  35563  nfded  35581  nfded2  35582  nfunidALT2  35583  lshpinN  35603  trlid0  36790  hdmap10lem  38453  renegid  38669  repncan3  38680  islssfg2  39101  areaquad  39253  fperdvper  41663  itgvol0  41713  stoweidlem13  41759  stoweidlem26  41772  stoweidlem34  41780  wallispilem4  41814  dirkercncflem1  41849  dirkercncflem3  41851  dirkercncflem4  41852  fourierdlem35  41888  fourierdlem73  41925  funressndmafv2rn  42858  dfatbrafv2b  42880  fnbrafv2b  42883  ichnfimlem2  43022  lighneallem4b  43172  sbgoldbwt  43340  sbgoldbalt  43344  nnsum4primeseven  43363  nnsum4primesevenALTV  43364  bgoldbtbndlem1  43368  bgoldbtbndlem3  43370