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  1084  eqcomd  2746  nfabdwOLD  2933  eqvisset  3508  vtoclg  3566  vtocl  3570  vtoclOLD  3571  vtoclf  3576  vtoclgf  3581  vtoclg1f  3582  vtoclgOLD  3583  eueq3  3733  sbc2or  3813  csbiegf  3955  un00  4468  elimhyp  4613  elimhyp2v  4614  elimhyp3v  4615  elimhyp4v  4616  elimdhyp  4618  keephyp2v  4620  keephyp3v  4621  preq12b  4875  nfopd  4914  ssex  5339  opthwiener  5533  isso2i  5644  nfimad  6098  dfrel2  6220  ordtri3or  6427  on0eqel  6519  funsng  6629  cnvresid  6657  nffvd  6932  fnbrfvb  6973  fvelrnb  6982  fvelimab  6994  funfvop  7083  fvsnun2  7217  iunpw  7806  onsucuni  7864  onuninsuci  7877  tposf12  8292  oaword1  8608  oneo  8637  nnaword1  8685  nnneo  8711  naddword1  8747  1sdom2dom  9310  inficl  9494  fipwuni  9495  infeq5i  9705  cantnflt  9741  cantnflem1  9758  cnfcom  9769  brttrcl  9782  rankidn  9891  rankr1id  9931  rankxpsuc  9951  iscard  10044  iscard2  10045  carduni  10050  cardmin2  10068  infxpenlem  10082  alephgeom  10151  cardaleph  10158  infenaleph  10160  iscard3  10162  alephsson  10169  alephfp  10177  alephval3  10179  dfac12k  10217  axdc3lem2  10520  alephval2  10641  alephreg  10651  cfpwsdom  10653  alephom  10654  axrepndlem1  10661  axunndlem1  10664  axunnd  10665  axpowndlem2  10667  axpowndlem3  10668  axpowndlem4  10669  axpownd  10670  axregndlem2  10672  axinfndlem1  10674  axinfnd  10675  axacndlem4  10679  axacndlem5  10680  axacnd  10681  gchaleph2  10741  elwina  10755  elina  10756  winaon  10757  inawina  10759  winainf  10763  winalim  10764  tskr1om2  10837  r1tskina  10851  gruina  10887  grur1a  10888  indpi  10976  nqerrel  11001  recidnq  11034  ltaddnq  11043  pncan3  11544  divcan2  11957  ltp1  12134  ltm1  12136  recreclt  12194  elnn0z  12652  nn0ind-raph  12743  fzdifsuc  13644  2tnp1ge0ge0  13880  fsuppmapnn0fiubex  14043  faclbnd5  14347  hashfun  14486  ccatalpha  14641  caucvgrlem  15721  fsumcnv  15821  fprodcnv  16031  ef01bndlem  16232  sin01gt0  16238  cos01gt0  16239  egt2lt3  16254  cnso  16295  ltoddhalfle  16409  4sqlem12  17003  funcres  17960  fuchom  18030  fuchomOLD  18031  xpsmnd  18812  xpsgrp  19099  mulgfval  19109  mulgfvalALT  19110  nmznsg  19208  frgp0  19802  gsumval3lem2  19948  gsumval3  19949  xpsrngd  20206  xpsringd  20355  pwssplit1  21081  pzriprnglem4  21518  mvrf1  22029  psdmul  22193  ply1chr  22331  blssioo  24836  dvidlem  25970  dvcj  26008  dvrec  26013  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dv11cn  26060  dvivthlem2  26068  lhop1lem  26072  lhop1  26073  lhop2  26074  q1peqb  26215  pserdv  26491  sinhalfpilem  26523  tangtx  26565  efabl  26610  logi  26647  logneg2  26675  gausslemma2dlem1a  27427  lgseisenlem4  27440  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  dchrisum0lem3  27581  mulogsum  27594  pntrlog2bndlem1  27639  madebday  27956  sltp1d  28066  pncan3s  28121  divscan2wd  28240  om2noseqlt  28323  om2noseqoi  28327  n0sge0  28359  axlowdimlem7  28981  axlowdimlem10  28984  axcontlem6  29002  umgrbi  29136  rusgr1vtxlem  29623  clwwlknonwwlknonb  30138  3wlkond  30203  frcond3  30301  hsn0elch  31280  axpjcl  31432  omlsilem  31434  pjchi  31464  shs00i  31482  chj00i  31519  chabs1  31548  pjspansn  31609  chscllem1  31669  osumcor2i  31676  nonbooli  31683  atcvat4i  32429  xppreima  32664  xdivrec  32891  wrdt2ind  32920  psgndmfi  33091  sqsscirc1  33854  1stmbfm  34225  2ndmbfm  34226  carsgclctunlem2  34284  eulerpartlemgh  34343  hgt750leme  34635  bnj1148  34972  bnj1154  34975  fineqvpow  35072  fineqvacALT  35074  cvmlift3lem5  35291  cvmlift3lem7  35293  currybi  35656  dfon2lem3  35749  dfon2lem7  35753  distel  35767  altopthsn  35925  bj-ax12  36623  bj-exlimmpbi  36879  irrdiff  37292  rdgssun  37344  poimirlem9  37589  poimirlem26  37606  poimirlem27  37607  poimirlem32  37612  dvasin  37664  areacirclem4  37671  heiborlem8  37778  0rngo  37987  ax12eq  38897  ax12el  38898  ax12inda  38904  ax12v2-o  38905  nfded  38923  nfded2  38924  nfunidALT2  38925  lshpinN  38945  trlid0  40133  hdmap10lem  41796  lcmineqlem  42009  aks4d1p1p5  42032  metakunt24  42185  fisdomnn  42239  asin1half  42339  renegid  42349  repncan3  42359  sn-00idlem2  42375  reixi  42398  sn-ltp1  42440  flt4lem7  42614  islssfg2  43028  areaquad  43177  onsupuni  43190  onov0suclim  43236  minregex  43496  fperdvper  45840  itgvol0  45889  stoweidlem13  45934  stoweidlem26  45947  stoweidlem34  45955  wallispilem4  45989  dirkercncflem1  46024  dirkercncflem3  46026  dirkercncflem4  46027  fourierdlem35  46063  fourierdlem73  46100  funressndmafv2rn  47138  dfatbrafv2b  47160  fnbrafv2b  47163  ichnfimlem  47337  lighneallem4b  47483  sbgoldbwt  47651  sbgoldbalt  47655  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  bgoldbtbndlem3  47681  grimidvtxedg  47760  iooii  48597  0thincg  48717