Theorem mpbii 232

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  dedt  1082  eqcomd  2745  clelab  2884  nfabdwOLD  2932  eqvisset  3447  vtocl  3496  vtoclgf  3501  vtoclg1f  3502  vtoclg  3503  eueq3  3649  sbc2or  3728  csbiegf  3870  un00  4381  elimhyp  4529  elimhyp2v  4530  elimhyp3v  4531  elimhyp4v  4532  elimdhyp  4534  keephyp2v  4536  keephyp3v  4537  preq12b  4786  nfopd  4826  ssex  5248  opthwiener  5430  isso2i  5537  nfimad  5975  dfrel2  6089  ordtri3or  6295  on0eqel  6381  funsng  6481  cnvresid  6509  nffvd  6780  fnbrfvb  6816  fvelrnb  6824  fvelimab  6835  funfvop  6921  fvsnun2  7049  rnmptcOLD  7077  iunpw  7612  onsucuni  7663  onuninsuci  7675  tposf12  8051  oaword1  8359  oneo  8388  nnaword1  8436  nnneo  8459  inficl  9145  fipwuni  9146  infeq5i  9355  cantnflt  9391  cantnflem1  9408  cnfcom  9419  brttrcl  9432  rankidn  9564  rankr1id  9604  rankxpsuc  9624  iscard  9717  iscard2  9718  carduni  9723  cardmin2  9741  infxpenlem  9753  alephgeom  9822  cardaleph  9829  infenaleph  9831  iscard3  9833  alephsson  9840  alephfp  9848  alephval3  9850  dfac12k  9887  axdc3lem2  10191  alephval2  10312  alephreg  10322  cfpwsdom  10324  alephom  10325  axrepndlem1  10332  axunndlem1  10335  axunnd  10336  axpowndlem2  10338  axpowndlem3  10339  axpowndlem4  10340  axpownd  10341  axregndlem2  10343  axinfndlem1  10345  axinfnd  10346  axacndlem4  10350  axacndlem5  10351  axacnd  10352  gchaleph2  10412  elwina  10426  elina  10427  winaon  10428  inawina  10430  winainf  10434  winalim  10435  tskr1om2  10508  r1tskina  10522  gruina  10558  grur1a  10559  indpi  10647  nqerrel  10672  recidnq  10705  ltaddnq  10714  pncan3  11212  divcan2  11624  ltp1  11798  ltm1  11800  recreclt  11857  elnn0z  12315  nn0ind-raph  12403  fzdifsuc  13298  2tnp1ge0ge0  13530  fsuppmapnn0fiubex  13693  faclbnd5  13993  hashfun  14133  ccatalpha  14279  caucvgrlem  15365  fsumcnv  15466  fprodcnv  15674  ef01bndlem  15874  sin01gt0  15880  cos01gt0  15881  egt2lt3  15896  cnso  15937  ltoddhalfle  16051  4sqlem12  16638  funcres  17592  fuchom  17659  fuchomOLD  17660  xpsmnd  18406  xpsgrp  18675  mulgfval  18683  mulgfvalALT  18684  nmznsg  18777  frgp0  19347  gsumval3lem2  19488  gsumval3  19489  pwssplit1  20302  mvrf1  21175  blssioo  23939  dvidlem  25060  dvcj  25095  dvrec  25100  rolle  25135  cmvth  25136  mvth  25137  dvlip  25138  dvlipcn  25139  dv11cn  25146  dvivthlem2  25154  lhop1lem  25158  lhop1  25159  lhop2  25160  q1peqb  25300  pserdv  25569  sinhalfpilem  25601  tangtx  25643  efabl  25687  logneg2  25751  gausslemma2dlem1a  26494  lgseisenlem4  26507  2lgslem3a  26525  2lgslem3b  26526  2lgslem3c  26527  2lgslem3d  26528  dchrisum0lem3  26648  mulogsum  26661  pntrlog2bndlem1  26706  axlowdimlem7  27297  axlowdimlem10  27300  axcontlem6  27318  umgrbi  27452  rusgr1vtxlem  27935  clwwlknonwwlknonb  28449  3wlkond  28514  frcond3  28612  hsn0elch  29589  axpjcl  29741  omlsilem  29743  pjchi  29773  shs00i  29791  chj00i  29828  chabs1  29857  pjspansn  29918  chscllem1  29978  osumcor2i  29985  nonbooli  29992  atcvat4i  30738  xppreima  30962  xdivrec  31180  wrdt2ind  31204  psgndmfi  31344  ply1chr  31648  sqsscirc1  31837  1stmbfm  32206  2ndmbfm  32207  carsgclctunlem2  32265  eulerpartlemgh  32324  hgt750leme  32617  bnj1148  32955  bnj1154  32958  fineqvpow  33044  fineqvacALT  33046  cvmlift3lem5  33264  cvmlift3lem7  33266  logi  33679  dfon2lem3  33740  dfon2lem7  33744  distel  33758  madebday  34059  altopthsn  34242  bj-ax12  34817  bj-exlimmpbi  35077  irrdiff  35476  rdgssun  35528  poimirlem9  35765  poimirlem26  35782  poimirlem27  35783  poimirlem32  35788  dvasin  35840  areacirclem4  35847  heiborlem8  35955  0rngo  36164  ax12eq  36934  ax12el  36935  ax12inda  36941  ax12v2-o  36942  nfded  36960  nfded2  36961  nfunidALT2  36962  lshpinN  36982  trlid0  38169  hdmap10lem  39832  lcmineqlem  40040  aks4d1p1p5  40063  metakunt24  40128  renegid  40336  repncan3  40346  sn-00idlem2  40362  reixi  40384  sn-ltp1  40413  flt4lem7  40476  islssfg2  40876  areaquad  41027  fperdvper  43414  itgvol0  43463  stoweidlem13  43508  stoweidlem26  43521  stoweidlem34  43529  wallispilem4  43563  dirkercncflem1  43598  dirkercncflem3  43600  dirkercncflem4  43601  fourierdlem35  43637  fourierdlem73  43674  funressndmafv2rn  44666  dfatbrafv2b  44688  fnbrafv2b  44691  ichnfimlem  44867  lighneallem4b  45013  sbgoldbwt  45181  sbgoldbalt  45185  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  bgoldbtbndlem1  45209  bgoldbtbndlem3  45211  iooii  46163  0thincg  46283