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  2736  eqvisset  3470  vtoclg  3523  vtocl  3527  vtoclOLD  3528  vtoclf  3533  vtoclgf  3538  vtoclg1f  3539  vtoclgOLD  3540  eueq3  3685  sbc2or  3765  csbiegf  3898  un00  4411  elimhyp  4557  elimhyp2v  4558  elimhyp3v  4559  elimhyp4v  4560  elimdhyp  4562  keephyp2v  4564  keephyp3v  4565  preq12b  4817  nfopd  4857  ssex  5279  opthwiener  5477  isso2i  5586  nfimad  6043  dfrel2  6165  ordtri3or  6367  on0eqel  6461  funsng  6570  cnvresid  6598  nffvd  6873  fnbrfvb  6914  fvelrnb  6924  fvelimab  6936  funfvop  7025  fvsnun2  7160  iunpw  7750  onsucuni  7806  onuninsuci  7819  tposf12  8233  oaword1  8519  oneo  8548  nnaword1  8596  nnneo  8622  naddword1  8658  1sdom2dom  9201  inficl  9383  fipwuni  9384  infeq5i  9596  cantnflt  9632  cantnflem1  9649  cnfcom  9660  brttrcl  9673  rankidn  9782  rankr1id  9822  rankxpsuc  9842  iscard  9935  iscard2  9936  carduni  9941  cardmin2  9959  infxpenlem  9973  alephgeom  10042  cardaleph  10049  infenaleph  10051  iscard3  10053  alephsson  10060  alephfp  10068  alephval3  10070  dfac12k  10108  axdc3lem2  10411  alephval2  10532  alephreg  10542  cfpwsdom  10544  alephom  10545  axrepndlem1  10552  axunndlem1  10555  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axpownd  10561  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  gchaleph2  10632  elwina  10646  elina  10647  winaon  10648  inawina  10650  winainf  10654  winalim  10655  tskr1om2  10728  r1tskina  10742  gruina  10778  grur1a  10779  indpi  10867  nqerrel  10892  recidnq  10925  ltaddnq  10934  pncan3  11436  divcan2  11852  ltp1  12029  ltm1  12031  recreclt  12089  elnn0z  12549  nn0ind-raph  12641  fzdifsuc  13552  2tnp1ge0ge0  13798  fsuppmapnn0fiubex  13964  faclbnd5  14270  hashfun  14409  ccatalpha  14565  caucvgrlem  15646  fsumcnv  15746  fprodcnv  15956  ef01bndlem  16159  sin01gt0  16165  cos01gt0  16166  egt2lt3  16181  cnso  16222  ltoddhalfle  16338  4sqlem12  16934  funcres  17865  fuchom  17933  xpsmnd  18711  xpsgrp  18998  mulgfval  19008  mulgfvalALT  19009  nmznsg  19107  frgp0  19697  gsumval3lem2  19843  gsumval3  19844  xpsrngd  20095  xpsringd  20248  pwssplit1  20973  pzriprnglem4  21401  mvrf1  21902  psdmul  22060  ply1chr  22200  blssioo  24690  dvidlem  25823  dvcj  25861  dvrec  25866  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlipcn  25906  dv11cn  25913  dvivthlem2  25921  lhop1lem  25925  lhop1  25926  lhop2  25927  q1peqb  26068  pserdv  26346  sinhalfpilem  26379  tangtx  26421  efabl  26466  logi  26503  logneg2  26531  gausslemma2dlem1a  27283  lgseisenlem4  27296  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  dchrisum0lem3  27437  mulogsum  27450  pntrlog2bndlem1  27495  madebday  27818  sltp1d  27929  pncan3s  27984  divscan2wd  28107  om2noseqoi  28204  n0sge0  28237  axlowdimlem7  28882  axlowdimlem10  28885  axcontlem6  28903  umgrbi  29035  rusgr1vtxlem  29522  clwwlknonwwlknonb  30042  3wlkond  30107  frcond3  30205  hsn0elch  31184  axpjcl  31336  omlsilem  31338  pjchi  31368  shs00i  31386  chj00i  31423  chabs1  31452  pjspansn  31513  chscllem1  31573  osumcor2i  31580  nonbooli  31587  atcvat4i  32333  xppreima  32576  xdivrec  32854  wrdt2ind  32882  psgndmfi  33062  sqsscirc1  33905  1stmbfm  34258  2ndmbfm  34259  carsgclctunlem2  34317  eulerpartlemgh  34376  hgt750leme  34656  bnj1148  34993  bnj1154  34996  fineqvpow  35093  fineqvacALT  35095  cvmlift3lem5  35317  cvmlift3lem7  35319  currybi  35682  dfon2lem3  35780  dfon2lem7  35784  distel  35798  altopthsn  35956  bj-ax12  36652  bj-exlimmpbi  36908  irrdiff  37321  rdgssun  37373  wl-ax12v2cl  37501  poimirlem9  37630  poimirlem26  37647  poimirlem27  37648  poimirlem32  37653  dvasin  37705  areacirclem4  37712  heiborlem8  37819  0rngo  38028  ax12eq  38941  ax12el  38942  ax12inda  38948  ax12v2-o  38949  nfded  38967  nfded2  38968  nfunidALT2  38969  lshpinN  38989  trlid0  40177  hdmap10lem  41840  lcmineqlem  42047  aks4d1p1p5  42070  fisdomnn  42239  asin1half  42352  renegid  42368  repncan3  42378  sn-00idlem2  42394  reixi  42418  sn-ltp1  42471  flt4lem7  42654  islssfg2  43067  areaquad  43212  onsupuni  43225  onov0suclim  43270  minregex  43530  wfac8prim  44999  fperdvper  45924  itgvol0  45973  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  wallispilem4  46073  dirkercncflem1  46108  dirkercncflem3  46110  dirkercncflem4  46111  fourierdlem35  46147  fourierdlem73  46184  funressndmafv2rn  47228  dfatbrafv2b  47250  fnbrafv2b  47253  ichnfimlem  47468  lighneallem4b  47614  sbgoldbwt  47782  sbgoldbalt  47786  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbndlem1  47810  bgoldbtbndlem3  47812  grimidvtxedg  47889  tposideq  48880  iooii  48910  0thincg  49451  oduoppcciso  49559