Theorem mpbii 232

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  dedt  1084  eqcomd  2743  clelab  2881  nfabdwOLD  2929  eqvisset  3459  vtocl  3510  vtoclgf  3515  vtoclg1f  3516  vtoclg  3517  eueq3  3660  sbc2or  3739  csbiegf  3880  un00  4393  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elimdhyp  4547  keephyp2v  4549  keephyp3v  4550  preq12b  4799  nfopd  4838  ssex  5269  opthwiener  5462  isso2i  5571  nfimad  6012  dfrel2  6131  ordtri3or  6338  on0eqel  6428  funsng  6539  cnvresid  6567  nffvd  6841  fnbrfvb  6882  fvelrnb  6890  fvelimab  6901  funfvop  6987  fvsnun2  7115  rnmptcOLD  7143  iunpw  7687  onsucuni  7745  onuninsuci  7758  tposf12  8141  oaword1  8458  oneo  8487  nnaword1  8535  nnneo  8560  1sdom2dom  9116  inficl  9286  fipwuni  9287  infeq5i  9497  cantnflt  9533  cantnflem1  9550  cnfcom  9561  brttrcl  9574  rankidn  9683  rankr1id  9723  rankxpsuc  9743  iscard  9836  iscard2  9837  carduni  9842  cardmin2  9860  infxpenlem  9874  alephgeom  9943  cardaleph  9950  infenaleph  9952  iscard3  9954  alephsson  9961  alephfp  9969  alephval3  9971  dfac12k  10008  axdc3lem2  10312  alephval2  10433  alephreg  10443  cfpwsdom  10445  alephom  10446  axrepndlem1  10453  axunndlem1  10456  axunnd  10457  axpowndlem2  10459  axpowndlem3  10460  axpowndlem4  10461  axpownd  10462  axregndlem2  10464  axinfndlem1  10466  axinfnd  10467  axacndlem4  10471  axacndlem5  10472  axacnd  10473  gchaleph2  10533  elwina  10547  elina  10548  winaon  10549  inawina  10551  winainf  10555  winalim  10556  tskr1om2  10629  r1tskina  10643  gruina  10679  grur1a  10680  indpi  10768  nqerrel  10793  recidnq  10826  ltaddnq  10835  pncan3  11334  divcan2  11746  ltp1  11920  ltm1  11922  recreclt  11979  elnn0z  12437  nn0ind-raph  12525  fzdifsuc  13421  2tnp1ge0ge0  13654  fsuppmapnn0fiubex  13817  faclbnd5  14117  hashfun  14256  ccatalpha  14400  caucvgrlem  15483  fsumcnv  15584  fprodcnv  15792  ef01bndlem  15992  sin01gt0  15998  cos01gt0  15999  egt2lt3  16014  cnso  16055  ltoddhalfle  16169  4sqlem12  16754  funcres  17708  fuchom  17775  fuchomOLD  17776  xpsmnd  18522  xpsgrp  18790  mulgfval  18798  mulgfvalALT  18799  nmznsg  18892  frgp0  19461  gsumval3lem2  19601  gsumval3  19602  pwssplit1  20426  mvrf1  21299  blssioo  24063  dvidlem  25184  dvcj  25219  dvrec  25224  rolle  25259  cmvth  25260  mvth  25261  dvlip  25262  dvlipcn  25263  dv11cn  25270  dvivthlem2  25278  lhop1lem  25282  lhop1  25283  lhop2  25284  q1peqb  25424  pserdv  25693  sinhalfpilem  25725  tangtx  25767  efabl  25811  logneg2  25875  gausslemma2dlem1a  26618  lgseisenlem4  26631  2lgslem3a  26649  2lgslem3b  26650  2lgslem3c  26651  2lgslem3d  26652  dchrisum0lem3  26772  mulogsum  26785  pntrlog2bndlem1  26830  axlowdimlem7  27604  axlowdimlem10  27607  axcontlem6  27625  umgrbi  27759  rusgr1vtxlem  28242  clwwlknonwwlknonb  28757  3wlkond  28822  frcond3  28920  hsn0elch  29897  axpjcl  30049  omlsilem  30051  pjchi  30081  shs00i  30099  chj00i  30136  chabs1  30165  pjspansn  30226  chscllem1  30286  osumcor2i  30293  nonbooli  30300  atcvat4i  31046  xppreima  31268  xdivrec  31486  wrdt2ind  31510  psgndmfi  31650  ply1chr  31964  sqsscirc1  32154  1stmbfm  32525  2ndmbfm  32526  carsgclctunlem2  32584  eulerpartlemgh  32643  hgt750leme  32936  bnj1148  33273  bnj1154  33276  fineqvpow  33362  fineqvacALT  33364  cvmlift3lem5  33582  cvmlift3lem7  33584  logi  33990  dfon2lem3  34044  dfon2lem7  34048  distel  34062  naddword1  34128  madebday  34188  altopthsn  34400  bj-ax12  34975  bj-exlimmpbi  35234  irrdiff  35651  rdgssun  35703  poimirlem9  35942  poimirlem26  35959  poimirlem27  35960  poimirlem32  35965  dvasin  36017  areacirclem4  36024  heiborlem8  36132  0rngo  36341  ax12eq  37259  ax12el  37260  ax12inda  37266  ax12v2-o  37267  nfded  37285  nfded2  37286  nfunidALT2  37287  lshpinN  37307  trlid0  38495  hdmap10lem  40158  lcmineqlem  40365  aks4d1p1p5  40388  metakunt24  40456  renegid  40667  repncan3  40677  sn-00idlem2  40693  reixi  40715  sn-ltp1  40744  flt4lem7  40809  islssfg2  41210  areaquad  41362  minregex  41515  fperdvper  43848  itgvol0  43897  stoweidlem13  43942  stoweidlem26  43955  stoweidlem34  43963  wallispilem4  43997  dirkercncflem1  44032  dirkercncflem3  44034  dirkercncflem4  44035  fourierdlem35  44071  fourierdlem73  44108  funressndmafv2rn  45133  dfatbrafv2b  45155  fnbrafv2b  45158  ichnfimlem  45333  lighneallem4b  45479  sbgoldbwt  45647  sbgoldbalt  45651  nnsum4primeseven  45670  nnsum4primesevenALTV  45671  bgoldbtbndlem1  45675  bgoldbtbndlem3  45677  iooii  46629  0thincg  46749