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  3467  vtoclg  3520  vtocl  3524  vtoclOLD  3525  vtoclf  3530  vtoclgf  3535  vtoclg1f  3536  vtoclgOLD  3537  eueq3  3682  sbc2or  3762  csbiegf  3895  un00  4408  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elimdhyp  4559  keephyp2v  4561  keephyp3v  4562  preq12b  4814  nfopd  4854  ssex  5276  opthwiener  5474  isso2i  5583  nfimad  6040  dfrel2  6162  ordtri3or  6364  on0eqel  6458  funsng  6567  cnvresid  6595  nffvd  6870  fnbrfvb  6911  fvelrnb  6921  fvelimab  6933  funfvop  7022  fvsnun2  7157  iunpw  7747  onsucuni  7803  onuninsuci  7816  tposf12  8230  oaword1  8516  oneo  8545  nnaword1  8593  nnneo  8619  naddword1  8655  1sdom2dom  9194  inficl  9376  fipwuni  9377  infeq5i  9589  cantnflt  9625  cantnflem1  9642  cnfcom  9653  brttrcl  9666  rankidn  9775  rankr1id  9815  rankxpsuc  9835  iscard  9928  iscard2  9929  carduni  9934  cardmin2  9952  infxpenlem  9966  alephgeom  10035  cardaleph  10042  infenaleph  10044  iscard3  10046  alephsson  10053  alephfp  10061  alephval3  10063  dfac12k  10101  axdc3lem2  10404  alephval2  10525  alephreg  10535  cfpwsdom  10537  alephom  10538  axrepndlem1  10545  axunndlem1  10548  axunnd  10549  axpowndlem2  10551  axpowndlem3  10552  axpowndlem4  10553  axpownd  10554  axregndlem2  10556  axinfndlem1  10558  axinfnd  10559  axacndlem4  10563  axacndlem5  10564  axacnd  10565  gchaleph2  10625  elwina  10639  elina  10640  winaon  10641  inawina  10643  winainf  10647  winalim  10648  tskr1om2  10721  r1tskina  10735  gruina  10771  grur1a  10772  indpi  10860  nqerrel  10885  recidnq  10918  ltaddnq  10927  pncan3  11429  divcan2  11845  ltp1  12022  ltm1  12024  recreclt  12082  elnn0z  12542  nn0ind-raph  12634  fzdifsuc  13545  2tnp1ge0ge0  13791  fsuppmapnn0fiubex  13957  faclbnd5  14263  hashfun  14402  ccatalpha  14558  caucvgrlem  15639  fsumcnv  15739  fprodcnv  15949  ef01bndlem  16152  sin01gt0  16158  cos01gt0  16159  egt2lt3  16174  cnso  16215  ltoddhalfle  16331  4sqlem12  16927  funcres  17858  fuchom  17926  xpsmnd  18704  xpsgrp  18991  mulgfval  19001  mulgfvalALT  19002  nmznsg  19100  frgp0  19690  gsumval3lem2  19836  gsumval3  19837  xpsrngd  20088  xpsringd  20241  pwssplit1  20966  pzriprnglem4  21394  mvrf1  21895  psdmul  22053  ply1chr  22193  blssioo  24683  dvidlem  25816  dvcj  25854  dvrec  25859  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlipcn  25899  dv11cn  25906  dvivthlem2  25914  lhop1lem  25918  lhop1  25919  lhop2  25920  q1peqb  26061  pserdv  26339  sinhalfpilem  26372  tangtx  26414  efabl  26459  logi  26496  logneg2  26524  gausslemma2dlem1a  27276  lgseisenlem4  27289  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  dchrisum0lem3  27430  mulogsum  27443  pntrlog2bndlem1  27488  madebday  27811  sltp1d  27922  pncan3s  27977  divscan2wd  28100  om2noseqoi  28197  n0sge0  28230  axlowdimlem7  28875  axlowdimlem10  28878  axcontlem6  28896  umgrbi  29028  rusgr1vtxlem  29515  clwwlknonwwlknonb  30035  3wlkond  30100  frcond3  30198  hsn0elch  31177  axpjcl  31329  omlsilem  31331  pjchi  31361  shs00i  31379  chj00i  31416  chabs1  31445  pjspansn  31506  chscllem1  31566  osumcor2i  31573  nonbooli  31580  atcvat4i  32326  xppreima  32569  xdivrec  32847  wrdt2ind  32875  psgndmfi  33055  sqsscirc1  33898  1stmbfm  34251  2ndmbfm  34252  carsgclctunlem2  34310  eulerpartlemgh  34369  hgt750leme  34649  bnj1148  34986  bnj1154  34989  fineqvpow  35086  fineqvacALT  35088  cvmlift3lem5  35310  cvmlift3lem7  35312  currybi  35675  dfon2lem3  35773  dfon2lem7  35777  distel  35791  altopthsn  35949  bj-ax12  36645  bj-exlimmpbi  36901  irrdiff  37314  rdgssun  37366  wl-ax12v2cl  37494  poimirlem9  37623  poimirlem26  37640  poimirlem27  37641  poimirlem32  37646  dvasin  37698  areacirclem4  37705  heiborlem8  37812  0rngo  38021  ax12eq  38934  ax12el  38935  ax12inda  38941  ax12v2-o  38942  nfded  38960  nfded2  38961  nfunidALT2  38962  lshpinN  38982  trlid0  40170  hdmap10lem  41833  lcmineqlem  42040  aks4d1p1p5  42063  fisdomnn  42232  asin1half  42345  renegid  42361  repncan3  42371  sn-00idlem2  42387  reixi  42411  sn-ltp1  42464  flt4lem7  42647  islssfg2  43060  areaquad  43205  onsupuni  43218  onov0suclim  43263  minregex  43523  wfac8prim  44992  fperdvper  45917  itgvol0  45966  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  wallispilem4  46066  dirkercncflem1  46101  dirkercncflem3  46103  dirkercncflem4  46104  fourierdlem35  46140  fourierdlem73  46177  funressndmafv2rn  47224  dfatbrafv2b  47246  fnbrafv2b  47249  ichnfimlem  47464  lighneallem4b  47610  sbgoldbwt  47778  sbgoldbalt  47782  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  bgoldbtbndlem3  47808  grimidvtxedg  47885  tposideq  48876  iooii  48906  0thincg  49447  oduoppcciso  49555