Theorem mpbii 236

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  dedt  1100  eqcomd  2768  eqvisset  3473  vtoclg  3520  vtocl  3523  vtoclf  3528  vtoclgf  3532  vtoclg1f  3533  eueq3  3672  sbc2or  3751  csbiegf  3883  un00  4360  vvin  4362  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elimdhyp  4556  keephyp2v  4558  keephyp3v  4559  preq12b  4813  nfopd  4853  ssexOLD  5290  opthwiener  5495  isso2i  5604  nfimad  6069  dfrel2  6186  ordtri3or  6394  on0eqel  6487  funsng  6588  cnvresid  6616  nffvd  6894  fnbrfvb  6932  fvelrnb  6942  fvelimab  6954  funfvop  7046  fvsnun2  7185  iunpw  7774  onsucuni  7828  onuninsuci  7840  tposf12  8253  oaword1  8543  oneo  8572  nnaword1  8621  nnneo  8647  naddword1  8684  1sdom2dom  9228  inficl  9399  fipwuni  9400  infeq5i  9619  cantnflt  9655  cantnflem1  9672  cnfcom  9683  brttrcl  9696  rankidn  9808  rankr1id  9848  rankxpsuc  9868  iscard  9984  iscard2  9985  carduni  9990  cardmin2  10008  infxpenlem  10020  alephgeom  10089  cardaleph  10096  infenaleph  10098  iscard3  10100  alephsson  10107  alephfp  10115  alephval3  10117  dfac12k  10154  axdc3lem2  10457  alephval2  10585  alephreg  10595  cfpwsdom  10597  alephom  10598  axrepndlem1  10605  axunndlem1  10608  axunnd  10609  axpowndlem2  10611  axpowndlem3  10612  axpowndlem4  10613  axpownd  10614  axregndlem2  10616  axinfndlem1  10618  axinfnd  10619  axacndlem4  10623  axacndlem5  10624  axacnd  10625  gchaleph2  10685  elwina  10699  elina  10700  winaon  10701  inawina  10703  winainf  10707  winalim  10708  tskr1om2  10781  r1tskina  10795  gruina  10831  grur1a  10832  indpi  10920  nqerrel  10945  recidnq  10978  ltaddnq  10987  pncan3  11493  divcan2  11908  ltp1  12083  ltm1  12085  recreclt  12142  elnn0z  12632  nn0ind-raph  12725  fzdifsuc  13643  2tnp1ge0ge0  13894  fsuppmapnn0fiubex  14060  faclbnd5  14366  hashfun  14506  ccatalpha  14664  caucvgrlem  15764  fsumcnv  15863  fprodcnv  16076  ef01bndlem  16278  sin01gt0  16284  cos01gt0  16285  egt2lt3  16300  cnso  16341  ltoddhalfle  16457  4sqlem12  17054  funcres  17991  fuchom  18059  xpsmnd  18890  xpsgrp  19188  mulgfval  19198  mulgfvalALT  19199  nmznsg  19297  frgp0  19893  gsumval3lem2  20039  gsumval3  20040  xpsrngd  20320  xpsringd  20479  pwssplit1  21249  pzriprnglem4  21703  mvrf1  22206  psdmul  22400  ply1chr  22537  blssioo  25027  dvidlem  26149  dvcj  26184  dvrec  26189  rolle  26224  cmvth  26225  mvth  26226  dvlip  26227  dvlipcn  26228  dv11cn  26235  dvivthlem2  26243  lhop1lem  26247  lhop1  26248  lhop2  26249  q1peqb  26388  pserdv  26672  sinhalfpilem  26708  tangtx  26750  efabl  26795  logi  26832  logneg2  26860  gausslemma2dlem1a  27609  lgseisenlem4  27622  2lgslem3a  27640  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  dchrisum0lem3  27763  mulogsum  27776  pntrlog2bndlem1  27821  madebday  28173  ltsp1d  28288  pncan3s  28346  divscan2wd  28470  om2noseqoi  28576  n0sge0  28611  bdayfinbndlem1  28740  1reno  28770  prlngsymquadlem  29328  axlowdimlem7  29413  axlowdimlem10  29416  axcontlem6  29434  umgrbi  29566  rusgr1vtxlem  30055  clwwlknonwwlknonb  30584  3wlkond  30659  frcond3  30757  hsn0elch  31737  axpjcl  31889  omlsilem  31891  pjchi  31921  shs00i  31939  chj00i  31976  chabs1  32005  pjspansn  32066  chscllem1  32126  osumcor2i  32133  nonbooli  32140  atcvat4i  32886  xppreima  33126  xdivrec  33380  wrdt2ind  33403  psgndmfi  33546  sqsscirc1  34426  1stmbfm  34779  2ndmbfm  34780  carsgclctunlem2  34838  eulerpartlemgh  34897  hgt750leme  35174  bnj1148  35513  bnj1154  35516  fineqvpow  35649  fineqvacALT  35651  fineqvnttrclse  35658  fineqvr1ombregs  35672  cvmlift3lem5  35910  cvmlift3lem7  35912  currybi  36275  dfon2lem3  36370  dfon2lem7  36374  distel  36388  altopthsn  36549  axtcond  37105  ttc00  37135  bj-ax12  37395  bj-exlimmpbi  37664  irrdiff  38086  rdgssun  38140  wl-ax12v2cl  38268  poimirlem9  38386  poimirlem26  38403  poimirlem27  38404  poimirlem32  38409  dvasin  38461  areacirclem4  38468  heiborlem8  38576  0rngo  38785  dfsuccl4  39230  suceldisj  39574  ax12eq  39822  ax12el  39823  ax12inda  39829  ax12v2-o  39830  nfded  39848  nfded2  39849  nfunidALT2  39850  lshpinN  39870  trlid0  41057  hdmap10lem  42720  lcmineqlem  42926  aks4d1p1p5  42949  fisdomnn  43119  asin1half  43240  renegid  43256  repncan3  43266  sn-00idlem2  43282  reixi  43306  rerecne0d  43339  sn-ltp1  43372  flt4lem7  43513  islssfg2  43920  areaquad  44065  onsupuni  44078  onov0suclim  44123  minregex  44382  wfac8prim  45833  fperdvper  46755  itgvol0  46804  stoweidlem13  46849  stoweidlem26  46862  stoweidlem34  46870  wallispilem4  46904  dirkercncflem1  46939  dirkercncflem3  46941  dirkercncflem4  46942  fourierdlem35  46978  fourierdlem73  47015  goldratval  47762  funressndmafv2rn  48119  dfatbrafv2b  48141  fnbrafv2b  48144  ichnfimlem  48371  lighneallem4b  48520  nprmdvdsfacm1lem4  48534  sbgoldbwt  48701  sbgoldbalt  48705  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  bgoldbtbndlem1  48729  bgoldbtbndlem3  48731  grimidvtxedg  48809  tposideq  49822  iooii  49852  0thincg  50392  oduoppcciso  50500