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  2741  eqvisset  3479  vtoclg  3533  vtocl  3537  vtoclOLD  3538  vtoclf  3543  vtoclgf  3548  vtoclg1f  3549  vtoclgOLD  3550  eueq3  3694  sbc2or  3774  csbiegf  3907  un00  4420  elimhyp  4566  elimhyp2v  4567  elimhyp3v  4568  elimhyp4v  4569  elimdhyp  4571  keephyp2v  4573  keephyp3v  4574  preq12b  4826  nfopd  4866  ssex  5291  opthwiener  5489  isso2i  5598  nfimad  6056  dfrel2  6178  ordtri3or  6384  on0eqel  6477  funsng  6586  cnvresid  6614  nffvd  6887  fnbrfvb  6928  fvelrnb  6938  fvelimab  6950  funfvop  7039  fvsnun2  7174  iunpw  7763  onsucuni  7820  onuninsuci  7833  tposf12  8248  oaword1  8562  oneo  8591  nnaword1  8639  nnneo  8665  naddword1  8701  1sdom2dom  9253  inficl  9435  fipwuni  9436  infeq5i  9648  cantnflt  9684  cantnflem1  9701  cnfcom  9712  brttrcl  9725  rankidn  9834  rankr1id  9874  rankxpsuc  9894  iscard  9987  iscard2  9988  carduni  9993  cardmin2  10011  infxpenlem  10025  alephgeom  10094  cardaleph  10101  infenaleph  10103  iscard3  10105  alephsson  10112  alephfp  10120  alephval3  10122  dfac12k  10160  axdc3lem2  10463  alephval2  10584  alephreg  10594  cfpwsdom  10596  alephom  10597  axrepndlem1  10604  axunndlem1  10607  axunnd  10608  axpowndlem2  10610  axpowndlem3  10611  axpowndlem4  10612  axpownd  10613  axregndlem2  10615  axinfndlem1  10617  axinfnd  10618  axacndlem4  10622  axacndlem5  10623  axacnd  10624  gchaleph2  10684  elwina  10698  elina  10699  winaon  10700  inawina  10702  winainf  10706  winalim  10707  tskr1om2  10780  r1tskina  10794  gruina  10830  grur1a  10831  indpi  10919  nqerrel  10944  recidnq  10977  ltaddnq  10986  pncan3  11488  divcan2  11902  ltp1  12079  ltm1  12081  recreclt  12139  elnn0z  12599  nn0ind-raph  12691  fzdifsuc  13599  2tnp1ge0ge0  13844  fsuppmapnn0fiubex  14008  faclbnd5  14314  hashfun  14453  ccatalpha  14609  caucvgrlem  15687  fsumcnv  15787  fprodcnv  15997  ef01bndlem  16200  sin01gt0  16206  cos01gt0  16207  egt2lt3  16222  cnso  16263  ltoddhalfle  16378  4sqlem12  16974  funcres  17907  fuchom  17975  xpsmnd  18753  xpsgrp  19040  mulgfval  19050  mulgfvalALT  19051  nmznsg  19149  frgp0  19739  gsumval3lem2  19885  gsumval3  19886  xpsrngd  20137  xpsringd  20290  pwssplit1  21015  pzriprnglem4  21443  mvrf1  21944  psdmul  22102  ply1chr  22242  blssioo  24732  dvidlem  25866  dvcj  25904  dvrec  25909  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvlipcn  25949  dv11cn  25956  dvivthlem2  25964  lhop1lem  25968  lhop1  25969  lhop2  25970  q1peqb  26111  pserdv  26389  sinhalfpilem  26422  tangtx  26464  efabl  26509  logi  26546  logneg2  26574  gausslemma2dlem1a  27326  lgseisenlem4  27339  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  dchrisum0lem3  27480  mulogsum  27493  pntrlog2bndlem1  27538  madebday  27855  sltp1d  27965  pncan3s  28020  divscan2wd  28139  om2noseqlt  28222  om2noseqoi  28226  n0sge0  28258  axlowdimlem7  28873  axlowdimlem10  28876  axcontlem6  28894  umgrbi  29026  rusgr1vtxlem  29513  clwwlknonwwlknonb  30033  3wlkond  30098  frcond3  30196  hsn0elch  31175  axpjcl  31327  omlsilem  31329  pjchi  31359  shs00i  31377  chj00i  31414  chabs1  31443  pjspansn  31504  chscllem1  31564  osumcor2i  31571  nonbooli  31578  atcvat4i  32324  xppreima  32569  xdivrec  32847  wrdt2ind  32875  psgndmfi  33055  sqsscirc1  33885  1stmbfm  34238  2ndmbfm  34239  carsgclctunlem2  34297  eulerpartlemgh  34356  hgt750leme  34636  bnj1148  34973  bnj1154  34976  fineqvpow  35073  fineqvacALT  35075  cvmlift3lem5  35291  cvmlift3lem7  35293  currybi  35656  dfon2lem3  35749  dfon2lem7  35753  distel  35767  altopthsn  35925  bj-ax12  36621  bj-exlimmpbi  36877  irrdiff  37290  rdgssun  37342  wl-ax12v2cl  37470  poimirlem9  37599  poimirlem26  37616  poimirlem27  37617  poimirlem32  37622  dvasin  37674  areacirclem4  37681  heiborlem8  37788  0rngo  37997  ax12eq  38905  ax12el  38906  ax12inda  38912  ax12v2-o  38913  nfded  38931  nfded2  38932  nfunidALT2  38933  lshpinN  38953  trlid0  40141  hdmap10lem  41804  lcmineqlem  42011  aks4d1p1p5  42034  metakunt24  42187  fisdomnn  42242  asin1half  42347  renegid  42363  repncan3  42373  sn-00idlem2  42389  reixi  42412  sn-ltp1  42454  flt4lem7  42629  islssfg2  43042  areaquad  43187  onsupuni  43200  onov0suclim  43245  minregex  43505  wfac8prim  44975  fperdvper  45896  itgvol0  45945  stoweidlem13  45990  stoweidlem26  46003  stoweidlem34  46011  wallispilem4  46045  dirkercncflem1  46080  dirkercncflem3  46082  dirkercncflem4  46083  fourierdlem35  46119  fourierdlem73  46156  funressndmafv2rn  47200  dfatbrafv2b  47222  fnbrafv2b  47225  ichnfimlem  47425  lighneallem4b  47571  sbgoldbwt  47739  sbgoldbalt  47743  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbndlem1  47767  bgoldbtbndlem3  47769  grimidvtxedg  47846  tposideq  48811  iooii  48840  0thincg  49292  oduoppcciso  49391