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  3456  vtoclg  3509  vtocl  3513  vtoclOLD  3514  vtoclf  3519  vtoclgf  3524  vtoclg1f  3525  vtoclgOLD  3526  eueq3  3671  sbc2or  3751  csbiegf  3884  un00  4396  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elimdhyp  4547  keephyp2v  4549  keephyp3v  4550  preq12b  4801  nfopd  4841  ssex  5260  opthwiener  5457  isso2i  5564  nfimad  6020  dfrel2  6138  ordtri3or  6339  on0eqel  6432  funsng  6533  cnvresid  6561  nffvd  6834  fnbrfvb  6873  fvelrnb  6883  fvelimab  6895  funfvop  6984  fvsnun2  7119  iunpw  7707  onsucuni  7761  onuninsuci  7773  tposf12  8184  oaword1  8470  oneo  8499  nnaword1  8547  nnneo  8573  naddword1  8609  1sdom2dom  9143  inficl  9315  fipwuni  9316  infeq5i  9532  cantnflt  9568  cantnflem1  9585  cnfcom  9596  brttrcl  9609  rankidn  9718  rankr1id  9758  rankxpsuc  9778  iscard  9871  iscard2  9872  carduni  9877  cardmin2  9895  infxpenlem  9907  alephgeom  9976  cardaleph  9983  infenaleph  9985  iscard3  9987  alephsson  9994  alephfp  10002  alephval3  10004  dfac12k  10042  axdc3lem2  10345  alephval2  10466  alephreg  10476  cfpwsdom  10478  alephom  10479  axrepndlem1  10486  axunndlem1  10489  axunnd  10490  axpowndlem2  10492  axpowndlem3  10493  axpowndlem4  10494  axpownd  10495  axregndlem2  10497  axinfndlem1  10499  axinfnd  10500  axacndlem4  10504  axacndlem5  10505  axacnd  10506  gchaleph2  10566  elwina  10580  elina  10581  winaon  10582  inawina  10584  winainf  10588  winalim  10589  tskr1om2  10662  r1tskina  10676  gruina  10712  grur1a  10713  indpi  10801  nqerrel  10826  recidnq  10859  ltaddnq  10868  pncan3  11371  divcan2  11787  ltp1  11964  ltm1  11966  recreclt  12024  elnn0z  12484  nn0ind-raph  12576  fzdifsuc  13487  2tnp1ge0ge0  13733  fsuppmapnn0fiubex  13899  faclbnd5  14205  hashfun  14344  ccatalpha  14500  caucvgrlem  15580  fsumcnv  15680  fprodcnv  15890  ef01bndlem  16093  sin01gt0  16099  cos01gt0  16100  egt2lt3  16115  cnso  16156  ltoddhalfle  16272  4sqlem12  16868  funcres  17803  fuchom  17871  xpsmnd  18651  xpsgrp  18938  mulgfval  18948  mulgfvalALT  18949  nmznsg  19047  frgp0  19639  gsumval3lem2  19785  gsumval3  19786  xpsrngd  20064  xpsringd  20217  pwssplit1  20963  pzriprnglem4  21391  mvrf1  21893  psdmul  22051  ply1chr  22191  blssioo  24681  dvidlem  25814  dvcj  25852  dvrec  25857  rolle  25892  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvlipcn  25897  dv11cn  25904  dvivthlem2  25912  lhop1lem  25916  lhop1  25917  lhop2  25918  q1peqb  26059  pserdv  26337  sinhalfpilem  26370  tangtx  26412  efabl  26457  logi  26494  logneg2  26522  gausslemma2dlem1a  27274  lgseisenlem4  27287  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  dchrisum0lem3  27428  mulogsum  27441  pntrlog2bndlem1  27486  madebday  27814  sltp1d  27927  pncan3s  27982  divscan2wd  28105  om2noseqoi  28202  n0sge0  28235  axlowdimlem7  28893  axlowdimlem10  28896  axcontlem6  28914  umgrbi  29046  rusgr1vtxlem  29533  clwwlknonwwlknonb  30050  3wlkond  30115  frcond3  30213  hsn0elch  31192  axpjcl  31344  omlsilem  31346  pjchi  31376  shs00i  31394  chj00i  31431  chabs1  31460  pjspansn  31521  chscllem1  31581  osumcor2i  31588  nonbooli  31595  atcvat4i  32341  xppreima  32588  xdivrec  32867  wrdt2ind  32895  psgndmfi  33040  sqsscirc1  33875  1stmbfm  34228  2ndmbfm  34229  carsgclctunlem2  34287  eulerpartlemgh  34346  hgt750leme  34626  bnj1148  34963  bnj1154  34966  fineqvpow  35071  fineqvacALT  35073  fineqvnttrclse  35077  cvmlift3lem5  35300  cvmlift3lem7  35302  currybi  35665  dfon2lem3  35763  dfon2lem7  35767  distel  35781  altopthsn  35939  bj-ax12  36635  bj-exlimmpbi  36891  irrdiff  37304  rdgssun  37356  wl-ax12v2cl  37484  poimirlem9  37613  poimirlem26  37630  poimirlem27  37631  poimirlem32  37636  dvasin  37688  areacirclem4  37695  heiborlem8  37802  0rngo  38011  ax12eq  38924  ax12el  38925  ax12inda  38931  ax12v2-o  38932  nfded  38950  nfded2  38951  nfunidALT2  38952  lshpinN  38972  trlid0  40159  hdmap10lem  41822  lcmineqlem  42029  aks4d1p1p5  42052  fisdomnn  42221  asin1half  42334  renegid  42350  repncan3  42360  sn-00idlem2  42376  reixi  42400  sn-ltp1  42453  flt4lem7  42636  islssfg2  43048  areaquad  43193  onsupuni  43206  onov0suclim  43251  minregex  43511  wfac8prim  44980  fperdvper  45904  itgvol0  45953  stoweidlem13  45998  stoweidlem26  46011  stoweidlem34  46019  wallispilem4  46053  dirkercncflem1  46088  dirkercncflem3  46090  dirkercncflem4  46091  fourierdlem35  46127  fourierdlem73  46164  funressndmafv2rn  47211  dfatbrafv2b  47233  fnbrafv2b  47236  ichnfimlem  47451  lighneallem4b  47597  sbgoldbwt  47765  sbgoldbalt  47769  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  bgoldbtbndlem3  47795  grimidvtxedg  47873  tposideq  48876  iooii  48906  0thincg  49447  oduoppcciso  49555