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:  elimhOLD  1077  dedt  1078  eqcomd  2829  nfabdw  3002  eqvisset  3513  vtocl  3561  vtoclgf  3567  vtoclg1f  3568  vtoclg  3569  eueq3  3704  sbc2or  3783  csbiegf  3918  un00  4396  elimhyp  4532  elimhyp2v  4533  elimhyp3v  4534  elimhyp4v  4535  elimdhyp  4537  keephyp2v  4539  keephyp3v  4540  preq12b  4783  nfopd  4822  ssex  5227  opthwiener  5406  isso2i  5510  nfimad  5940  dfrel2  6048  ordtri3or  6225  on0eqel  6310  funsng  6407  cnvresid  6435  nffvd  6684  fnbrfvb  6720  fvelrnb  6728  fvelimab  6739  funfvop  6822  fvsnun2  6947  rnmptcOLD  6972  iunpw  7495  onsucuni  7545  onuninsuci  7557  tposf12  7919  oaword1  8180  oneo  8209  nnaword1  8257  nnneo  8280  inficl  8891  fipwuni  8892  infeq5i  9101  cantnflt  9137  cantnflem1  9154  cnfcom  9165  rankidn  9253  rankr1id  9293  rankxpsuc  9313  iscard  9406  iscard2  9407  carduni  9412  cardmin2  9429  infxpenlem  9441  alephgeom  9510  cardaleph  9517  infenaleph  9519  iscard3  9521  alephsson  9528  alephfp  9536  alephval3  9538  dfac12k  9575  axdc3lem2  9875  alephval2  9996  alephreg  10006  cfpwsdom  10008  alephom  10009  axrepndlem1  10016  axunndlem1  10019  axunnd  10020  axpowndlem2  10022  axpowndlem3  10023  axpowndlem4  10024  axpownd  10025  axregndlem2  10027  axinfndlem1  10029  axinfnd  10030  axacndlem4  10034  axacndlem5  10035  axacnd  10036  gchaleph2  10096  elwina  10110  elina  10111  winaon  10112  inawina  10114  winainf  10118  winalim  10119  tskr1om2  10192  r1tskina  10206  gruina  10242  grur1a  10243  indpi  10331  nqerrel  10356  recidnq  10389  ltaddnq  10398  pncan3  10896  divcan2  11308  ltp1  11482  ltm1  11484  recreclt  11541  elnn0z  11997  nn0ind-raph  12085  fzdifsuc  12970  2tnp1ge0ge0  13202  fsuppmapnn0fiubex  13363  faclbnd5  13661  hashfun  13801  ccatalpha  13949  caucvgrlem  15031  fsumcnv  15130  fprodcnv  15339  ef01bndlem  15539  sin01gt0  15545  cos01gt0  15546  egt2lt3  15561  cnso  15602  ltoddhalfle  15712  4sqlem12  16294  funcres  17168  fuchom  17233  xpsmnd  17953  xpsgrp  18220  mulgfval  18228  mulgfvalALT  18229  nmznsg  18322  frgp0  18888  gsumval3lem2  19028  gsumval3  19029  pwssplit1  19833  mvrf1  20207  blssioo  23405  dvidlem  24515  dvcj  24549  dvrec  24554  rolle  24589  cmvth  24590  mvth  24591  dvlip  24592  dvlipcn  24593  dv11cn  24600  dvivthlem2  24608  lhop1lem  24612  lhop1  24613  lhop2  24614  q1peqb  24750  pserdv  25019  sinhalfpilem  25051  tangtx  25093  efabl  25136  logneg2  25200  gausslemma2dlem1a  25943  lgseisenlem4  25956  2lgslem3a  25974  2lgslem3b  25975  2lgslem3c  25976  2lgslem3d  25977  dchrisum0lem3  26097  mulogsum  26110  pntrlog2bndlem1  26155  axlowdimlem7  26736  axlowdimlem10  26739  axcontlem6  26757  umgrbi  26888  rusgr1vtxlem  27371  clwwlknonwwlknonb  27887  3wlkond  27952  frcond3  28050  hsn0elch  29027  axpjcl  29179  omlsilem  29181  pjchi  29211  shs00i  29229  chj00i  29266  chabs1  29295  pjspansn  29356  chscllem1  29416  osumcor2i  29423  nonbooli  29430  atcvat4i  30176  xppreima  30396  xdivrec  30605  wrdt2ind  30629  psgndmfi  30742  sqsscirc1  31153  1stmbfm  31520  2ndmbfm  31521  carsgclctunlem2  31579  eulerpartlemgh  31638  hgt750leme  31931  bnj1148  32270  bnj1154  32273  cvmlift3lem5  32572  cvmlift3lem7  32574  logi  32968  dfon2lem3  33032  dfon2lem7  33036  distel  33050  altopthsn  33424  bj-ax12  33992  bj-exlimmpbi  34231  rdgssun  34661  poimirlem9  34903  poimirlem26  34920  poimirlem27  34921  poimirlem32  34926  dvasin  34980  areacirclem4  34987  heiborlem8  35098  0rngo  35307  ax12eq  36079  ax12el  36080  ax12inda  36086  ax12v2-o  36087  nfded  36105  nfded2  36106  nfunidALT2  36107  lshpinN  36127  trlid0  37314  hdmap10lem  38977  renegid  39210  repncan3  39220  sn-00idlem2  39236  sn-ltp1  39254  islssfg2  39678  areaquad  39830  fperdvper  42210  itgvol0  42260  stoweidlem13  42305  stoweidlem26  42318  stoweidlem34  42326  wallispilem4  42360  dirkercncflem1  42395  dirkercncflem3  42397  dirkercncflem4  42398  fourierdlem35  42434  fourierdlem73  42471  funressndmafv2rn  43429  dfatbrafv2b  43451  fnbrafv2b  43454  ichnfimlem2  43629  lighneallem4b  43781  sbgoldbwt  43949  sbgoldbalt  43953  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  bgoldbtbndlem1  43977  bgoldbtbndlem3  43979