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  2767  eqvisset  3471  vtoclg  3518  vtocl  3521  vtoclf  3526  vtoclgf  3530  vtoclg1f  3531  eueq3  3669  sbc2or  3748  csbiegf  3880  un00  4357  vvin  4359  elimhyp  4548  elimhyp2v  4549  elimhyp3v  4550  elimhyp4v  4551  elimdhyp  4553  keephyp2v  4555  keephyp3v  4556  preq12b  4810  nfopd  4850  ssexOLD  5283  opthwiener  5487  isso2i  5596  nfimad  6063  dfrel2  6180  ordtri3or  6388  on0eqel  6481  funsng  6583  cnvresid  6611  nffvd  6889  fnbrfvb  6927  fvelrnb  6937  fvelimab  6949  funfvop  7041  fvsnun2  7180  iunpw  7774  onsucuni  7828  onuninsuci  7840  tposf12  8252  oaword1  8544  oneo  8573  nnaword1  8622  nnneo  8648  naddword1  8685  1sdom2dom  9229  inficl  9401  fipwuni  9402  infeq5i  9621  cantnflt  9657  cantnflem1  9674  cnfcom  9685  brttrcl  9698  rankidn  9812  rankr1id  9859  rankxpsuc  9880  iscard  10037  iscard2  10038  carduni  10043  cardmin2  10061  infxpenlem  10073  alephgeom  10142  cardaleph  10149  infenaleph  10151  iscard3  10153  alephsson  10160  alephfp  10168  alephval3  10170  dfac12k  10207  axdc3lem2  10510  alephval2  10638  alephreg  10648  cfpwsdom  10650  alephom  10651  axrepndlem1  10658  axunndlem1  10661  axunnd  10662  axpowndlem2  10664  axpowndlem3  10665  axpowndlem4  10666  axpownd  10667  axregndlem2  10669  axinfndlem1  10671  axinfnd  10672  axacndlem4  10676  axacndlem5  10677  axacnd  10678  gchaleph2  10738  elwina  10752  elina  10753  winaon  10754  inawina  10756  winainf  10760  winalim  10761  tskhf  10834  r1tskina  10848  gruina  10884  grur1a  10885  indpi  10973  nqerrel  10998  recidnq  11031  ltaddnq  11040  pncan3  11546  divcan2  11963  ltp1  12138  ltm1  12140  recreclt  12197  elnn0z  12687  nn0ind-raph  12780  fzdifsuc  13698  2tnp1ge0ge0  13949  fsuppmapnn0fiubex  14115  faclbnd5  14422  hashfun  14562  ccatalpha  14720  caucvgrlem  15820  fsumcnv  15919  fprodcnv  16130  ef01bndlem  16332  sin01gt0  16338  cos01gt0  16339  egt2lt3  16354  cnso  16395  ltoddhalfle  16511  4sqlem12  17114  funcres  18051  fuchom  18119  xpsmnd  18951  xpsgrp  19249  mulgfval  19259  mulgfvalALT  19260  nmznsg  19358  frgp0  19954  gsumval3lem2  20100  gsumval3  20101  xpsrngd  20381  xpsringd  20542  pwssplit1  21314  pzriprnglem4  21770  mvrf1  22273  psdmul  22467  ply1chr  22604  blssioo  25094  dvidlem  26215  dvcj  26250  dvrec  26255  rolle  26290  cmvth  26291  mvth  26292  dvlip  26293  dvlipcn  26294  dv11cn  26301  dvivthlem2  26309  lhop1lem  26313  lhop1  26314  lhop2  26315  q1peqb  26454  pserdv  26738  sinhalfpilem  26774  tangtx  26816  efabl  26860  logi  26897  logneg2  26925  gausslemma2dlem1a  27674  lgseisenlem4  27687  2lgslem3a  27705  2lgslem3b  27706  2lgslem3c  27707  2lgslem3d  27708  dchrisum0lem3  27828  mulogsum  27841  pntrlog2bndlem1  27886  flt4lem7  27971  madebday  28268  ltsp1d  28383  pncan3s  28441  divscan2wd  28565  om2noseqoi  28671  n0sge0  28706  bdayfinbndlem1  28835  1reno  28865  prlngsymquadlem  29423  axlowdimlem7  29508  axlowdimlem10  29511  axcontlem6  29529  umgrbi  29661  rusgr1vtxlem  30150  clwwlknonwwlknonb  30679  3wlkond  30754  frcond3  30852  hsn0elch  31832  axpjcl  31984  omlsilem  31986  pjchi  32016  shs00i  32034  chj00i  32071  chabs1  32100  pjspansn  32161  chscllem1  32221  osumcor2i  32228  nonbooli  32235  atcvat4i  32981  xppreima  33221  xdivrec  33475  wrdt2ind  33498  psgndmfi  33641  sqsscirc1  34522  1stmbfm  34875  2ndmbfm  34876  carsgclctunlem2  34934  eulerpartlemgh  34993  hgt750leme  35270  bnj1148  35609  bnj1154  35612  fineqvpow  35756  fineqvacALT  35758  fineqvnttrclse  35765  fineqvr1ombregs  35779  cvmlift3lem5  36057  cvmlift3lem7  36059  currybi  36422  dfon2lem3  36517  dfon2lem7  36521  distel  36535  altopthsn  36696  axtcond  37236  ttc00  37266  bj-ax12  37526  bj-exlimmpbi  37795  irrdiff  38215  rdgssun  38269  wl-ax12v2cl  38397  poimirlem9  38515  poimirlem26  38532  poimirlem27  38533  poimirlem32  38538  dvasin  38590  areacirclem4  38597  heiborlem8  38720  0rngo  38929  dfsuccl4  39374  suceldisj  39718  ax12eq  39966  ax12el  39967  ax12inda  39973  ax12v2-o  39974  nfded  39992  nfded2  39993  nfunidALT2  39994  lshpinN  40014  trlid0  41201  hdmap10lem  42864  lcmineqlem  43070  aks4d1p1p5  43093  fisdomnn  43263  asin1half  43376  renegid  43392  repncan3  43402  sn-00idlem2  43418  reixi  43442  rerecne0d  43475  sn-ltp1  43508  islssfg2  44031  areaquad  44176  onsupuni  44189  onov0suclim  44234  minregex  44493  wfac8prim  45944  fperdvper  46873  itgvol0  46922  stoweidlem13  46967  stoweidlem26  46980  stoweidlem34  46988  wallispilem4  47022  dirkercncflem1  47057  dirkercncflem3  47059  dirkercncflem4  47060  fourierdlem35  47096  fourierdlem73  47133  goldratval  47880  funressndmafv2rn  48237  dfatbrafv2b  48259  fnbrafv2b  48262  ichnfimlem  48489  lighneallem4b  48638  nprmdvdsfacm1lem4  48652  sbgoldbwt  48819  sbgoldbalt  48823  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  bgoldbtbndlem1  48847  bgoldbtbndlem3  48849  grimidvtxedg  48927  tposideq  49940  iooii  49970  0thincg  50510  oduoppcciso  50618