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  2743  eqvisset  3500  vtoclg  3554  vtocl  3558  vtoclOLD  3559  vtoclf  3564  vtoclgf  3569  vtoclg1f  3570  vtoclgOLD  3571  eueq3  3717  sbc2or  3797  csbiegf  3932  un00  4445  elimhyp  4591  elimhyp2v  4592  elimhyp3v  4593  elimhyp4v  4594  elimdhyp  4596  keephyp2v  4598  keephyp3v  4599  preq12b  4850  nfopd  4890  ssex  5321  opthwiener  5519  isso2i  5629  nfimad  6087  dfrel2  6209  ordtri3or  6416  on0eqel  6508  funsng  6617  cnvresid  6645  nffvd  6918  fnbrfvb  6959  fvelrnb  6969  fvelimab  6981  funfvop  7070  fvsnun2  7203  iunpw  7791  onsucuni  7848  onuninsuci  7861  tposf12  8276  oaword1  8590  oneo  8619  nnaword1  8667  nnneo  8693  naddword1  8729  1sdom2dom  9283  inficl  9465  fipwuni  9466  infeq5i  9676  cantnflt  9712  cantnflem1  9729  cnfcom  9740  brttrcl  9753  rankidn  9862  rankr1id  9902  rankxpsuc  9922  iscard  10015  iscard2  10016  carduni  10021  cardmin2  10039  infxpenlem  10053  alephgeom  10122  cardaleph  10129  infenaleph  10131  iscard3  10133  alephsson  10140  alephfp  10148  alephval3  10150  dfac12k  10188  axdc3lem2  10491  alephval2  10612  alephreg  10622  cfpwsdom  10624  alephom  10625  axrepndlem1  10632  axunndlem1  10635  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axpownd  10641  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  gchaleph2  10712  elwina  10726  elina  10727  winaon  10728  inawina  10730  winainf  10734  winalim  10735  tskr1om2  10808  r1tskina  10822  gruina  10858  grur1a  10859  indpi  10947  nqerrel  10972  recidnq  11005  ltaddnq  11014  pncan3  11516  divcan2  11930  ltp1  12107  ltm1  12109  recreclt  12167  elnn0z  12626  nn0ind-raph  12718  fzdifsuc  13624  2tnp1ge0ge0  13869  fsuppmapnn0fiubex  14033  faclbnd5  14337  hashfun  14476  ccatalpha  14631  caucvgrlem  15709  fsumcnv  15809  fprodcnv  16019  ef01bndlem  16220  sin01gt0  16226  cos01gt0  16227  egt2lt3  16242  cnso  16283  ltoddhalfle  16398  4sqlem12  16994  funcres  17941  fuchom  18009  xpsmnd  18790  xpsgrp  19077  mulgfval  19087  mulgfvalALT  19088  nmznsg  19186  frgp0  19778  gsumval3lem2  19924  gsumval3  19925  xpsrngd  20176  xpsringd  20329  pwssplit1  21058  pzriprnglem4  21495  mvrf1  22006  psdmul  22170  ply1chr  22310  blssioo  24816  dvidlem  25950  dvcj  25988  dvrec  25993  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlipcn  26033  dv11cn  26040  dvivthlem2  26048  lhop1lem  26052  lhop1  26053  lhop2  26054  q1peqb  26195  pserdv  26473  sinhalfpilem  26505  tangtx  26547  efabl  26592  logi  26629  logneg2  26657  gausslemma2dlem1a  27409  lgseisenlem4  27422  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  dchrisum0lem3  27563  mulogsum  27576  pntrlog2bndlem1  27621  madebday  27938  sltp1d  28048  pncan3s  28103  divscan2wd  28222  om2noseqlt  28305  om2noseqoi  28309  n0sge0  28341  axlowdimlem7  28963  axlowdimlem10  28966  axcontlem6  28984  umgrbi  29118  rusgr1vtxlem  29605  clwwlknonwwlknonb  30125  3wlkond  30190  frcond3  30288  hsn0elch  31267  axpjcl  31419  omlsilem  31421  pjchi  31451  shs00i  31469  chj00i  31506  chabs1  31535  pjspansn  31596  chscllem1  31656  osumcor2i  31663  nonbooli  31670  atcvat4i  32416  xppreima  32655  xdivrec  32909  wrdt2ind  32938  psgndmfi  33118  sqsscirc1  33907  1stmbfm  34262  2ndmbfm  34263  carsgclctunlem2  34321  eulerpartlemgh  34380  hgt750leme  34673  bnj1148  35010  bnj1154  35013  fineqvpow  35110  fineqvacALT  35112  cvmlift3lem5  35328  cvmlift3lem7  35330  currybi  35693  dfon2lem3  35786  dfon2lem7  35790  distel  35804  altopthsn  35962  bj-ax12  36658  bj-exlimmpbi  36914  irrdiff  37327  rdgssun  37379  wl-ax12v2cl  37507  poimirlem9  37636  poimirlem26  37653  poimirlem27  37654  poimirlem32  37659  dvasin  37711  areacirclem4  37718  heiborlem8  37825  0rngo  38034  ax12eq  38942  ax12el  38943  ax12inda  38949  ax12v2-o  38950  nfded  38968  nfded2  38969  nfunidALT2  38970  lshpinN  38990  trlid0  40178  hdmap10lem  41841  lcmineqlem  42053  aks4d1p1p5  42076  metakunt24  42229  fisdomnn  42285  asin1half  42387  renegid  42403  repncan3  42413  sn-00idlem2  42429  reixi  42452  sn-ltp1  42494  flt4lem7  42669  islssfg2  43083  areaquad  43228  onsupuni  43241  onov0suclim  43287  minregex  43547  wfac8prim  45019  fperdvper  45934  itgvol0  45983  stoweidlem13  46028  stoweidlem26  46041  stoweidlem34  46049  wallispilem4  46083  dirkercncflem1  46118  dirkercncflem3  46120  dirkercncflem4  46121  fourierdlem35  46157  fourierdlem73  46194  funressndmafv2rn  47235  dfatbrafv2b  47257  fnbrafv2b  47260  ichnfimlem  47450  lighneallem4b  47596  sbgoldbwt  47764  sbgoldbalt  47768  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbndlem1  47792  bgoldbtbndlem3  47794  grimidvtxedg  47876  tposideq  48788  iooii  48815  0thincg  49107  oduoppcciso  49170