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  1083  eqcomd  2735  eqvisset  3458  vtoclg  3511  vtocl  3515  vtoclOLD  3516  vtoclf  3521  vtoclgf  3526  vtoclg1f  3527  vtoclgOLD  3528  eueq3  3673  sbc2or  3753  csbiegf  3886  un00  4398  elimhyp  4544  elimhyp2v  4545  elimhyp3v  4546  elimhyp4v  4547  elimdhyp  4549  keephyp2v  4551  keephyp3v  4552  preq12b  4804  nfopd  4844  ssex  5263  opthwiener  5461  isso2i  5568  nfimad  6024  dfrel2  6142  ordtri3or  6343  on0eqel  6436  funsng  6537  cnvresid  6565  nffvd  6838  fnbrfvb  6877  fvelrnb  6887  fvelimab  6899  funfvop  6988  fvsnun2  7123  iunpw  7711  onsucuni  7767  onuninsuci  7780  tposf12  8191  oaword1  8477  oneo  8506  nnaword1  8554  nnneo  8580  naddword1  8616  1sdom2dom  9153  inficl  9334  fipwuni  9335  infeq5i  9551  cantnflt  9587  cantnflem1  9604  cnfcom  9615  brttrcl  9628  rankidn  9737  rankr1id  9777  rankxpsuc  9797  iscard  9890  iscard2  9891  carduni  9896  cardmin2  9914  infxpenlem  9926  alephgeom  9995  cardaleph  10002  infenaleph  10004  iscard3  10006  alephsson  10013  alephfp  10021  alephval3  10023  dfac12k  10061  axdc3lem2  10364  alephval2  10485  alephreg  10495  cfpwsdom  10497  alephom  10498  axrepndlem1  10505  axunndlem1  10508  axunnd  10509  axpowndlem2  10511  axpowndlem3  10512  axpowndlem4  10513  axpownd  10514  axregndlem2  10516  axinfndlem1  10518  axinfnd  10519  axacndlem4  10523  axacndlem5  10524  axacnd  10525  gchaleph2  10585  elwina  10599  elina  10600  winaon  10601  inawina  10603  winainf  10607  winalim  10608  tskr1om2  10681  r1tskina  10695  gruina  10731  grur1a  10732  indpi  10820  nqerrel  10845  recidnq  10878  ltaddnq  10887  pncan3  11389  divcan2  11805  ltp1  11982  ltm1  11984  recreclt  12042  elnn0z  12502  nn0ind-raph  12594  fzdifsuc  13505  2tnp1ge0ge0  13751  fsuppmapnn0fiubex  13917  faclbnd5  14223  hashfun  14362  ccatalpha  14518  caucvgrlem  15598  fsumcnv  15698  fprodcnv  15908  ef01bndlem  16111  sin01gt0  16117  cos01gt0  16118  egt2lt3  16133  cnso  16174  ltoddhalfle  16290  4sqlem12  16886  funcres  17821  fuchom  17889  xpsmnd  18669  xpsgrp  18956  mulgfval  18966  mulgfvalALT  18967  nmznsg  19065  frgp0  19657  gsumval3lem2  19803  gsumval3  19804  xpsrngd  20082  xpsringd  20235  pwssplit1  20981  pzriprnglem4  21409  mvrf1  21911  psdmul  22069  ply1chr  22209  blssioo  24699  dvidlem  25832  dvcj  25870  dvrec  25875  rolle  25910  cmvth  25911  cmvthOLD  25912  mvth  25913  dvlip  25914  dvlipcn  25915  dv11cn  25922  dvivthlem2  25930  lhop1lem  25934  lhop1  25935  lhop2  25936  q1peqb  26077  pserdv  26355  sinhalfpilem  26388  tangtx  26430  efabl  26475  logi  26512  logneg2  26540  gausslemma2dlem1a  27292  lgseisenlem4  27305  2lgslem3a  27323  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  dchrisum0lem3  27446  mulogsum  27459  pntrlog2bndlem1  27504  madebday  27832  sltp1d  27945  pncan3s  28000  divscan2wd  28123  om2noseqoi  28220  n0sge0  28253  axlowdimlem7  28911  axlowdimlem10  28914  axcontlem6  28932  umgrbi  29064  rusgr1vtxlem  29551  clwwlknonwwlknonb  30068  3wlkond  30133  frcond3  30231  hsn0elch  31210  axpjcl  31362  omlsilem  31364  pjchi  31394  shs00i  31412  chj00i  31449  chabs1  31478  pjspansn  31539  chscllem1  31599  osumcor2i  31606  nonbooli  31613  atcvat4i  32359  xppreima  32602  xdivrec  32880  wrdt2ind  32908  psgndmfi  33053  sqsscirc1  33874  1stmbfm  34227  2ndmbfm  34228  carsgclctunlem2  34286  eulerpartlemgh  34345  hgt750leme  34625  bnj1148  34962  bnj1154  34965  fineqvpow  35070  fineqvacALT  35072  cvmlift3lem5  35295  cvmlift3lem7  35297  currybi  35660  dfon2lem3  35758  dfon2lem7  35762  distel  35776  altopthsn  35934  bj-ax12  36630  bj-exlimmpbi  36886  irrdiff  37299  rdgssun  37351  wl-ax12v2cl  37479  poimirlem9  37608  poimirlem26  37625  poimirlem27  37626  poimirlem32  37631  dvasin  37683  areacirclem4  37690  heiborlem8  37797  0rngo  38006  ax12eq  38919  ax12el  38920  ax12inda  38926  ax12v2-o  38927  nfded  38945  nfded2  38946  nfunidALT2  38947  lshpinN  38967  trlid0  40155  hdmap10lem  41818  lcmineqlem  42025  aks4d1p1p5  42048  fisdomnn  42217  asin1half  42330  renegid  42346  repncan3  42356  sn-00idlem2  42372  reixi  42396  sn-ltp1  42449  flt4lem7  42632  islssfg2  43044  areaquad  43189  onsupuni  43202  onov0suclim  43247  minregex  43507  wfac8prim  44976  fperdvper  45901  itgvol0  45950  stoweidlem13  45995  stoweidlem26  46008  stoweidlem34  46016  wallispilem4  46050  dirkercncflem1  46085  dirkercncflem3  46087  dirkercncflem4  46088  fourierdlem35  46124  fourierdlem73  46161  funressndmafv2rn  47208  dfatbrafv2b  47230  fnbrafv2b  47233  ichnfimlem  47448  lighneallem4b  47594  sbgoldbwt  47762  sbgoldbalt  47766  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  bgoldbtbndlem1  47790  bgoldbtbndlem3  47792  grimidvtxedg  47870  tposideq  48873  iooii  48903  0thincg  49444  oduoppcciso  49552