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  2772  eqvisset  3478  vtoclg  3525  vtocl  3528  vtoclf  3533  vtoclgf  3537  vtoclg1f  3538  eueq3  3677  sbc2or  3756  csbiegf  3889  un00  4367  vvin  4369  elimhyp  4558  elimhyp2v  4559  elimhyp3v  4560  elimhyp4v  4561  elimdhyp  4563  keephyp2v  4565  keephyp3v  4566  preq12b  4820  nfopd  4860  ssexOLD  5297  opthwiener  5502  isso2i  5611  nfimad  6076  dfrel2  6192  ordtri3or  6400  on0eqel  6493  funsng  6594  cnvresid  6622  nffvd  6900  fnbrfvb  6938  fvelrnb  6948  fvelimab  6960  funfvop  7052  fvsnun2  7188  iunpw  7779  onsucuni  7833  onuninsuci  7845  tposf12  8256  oaword1  8546  oneo  8575  nnaword1  8624  nnneo  8650  naddword1  8687  1sdom2dom  9224  inficl  9395  fipwuni  9396  infeq5i  9615  cantnflt  9651  cantnflem1  9668  cnfcom  9679  brttrcl  9692  rankidn  9804  rankr1id  9844  rankxpsuc  9864  iscard  9980  iscard2  9981  carduni  9986  cardmin2  10004  infxpenlem  10016  alephgeom  10085  cardaleph  10092  infenaleph  10094  iscard3  10096  alephsson  10103  alephfp  10111  alephval3  10113  dfac12k  10150  axdc3lem2  10453  alephval2  10575  alephreg  10585  cfpwsdom  10587  alephom  10588  axrepndlem1  10595  axunndlem1  10598  axunnd  10599  axpowndlem2  10601  axpowndlem3  10602  axpowndlem4  10603  axpownd  10604  axregndlem2  10606  axinfndlem1  10608  axinfnd  10609  axacndlem4  10613  axacndlem5  10614  axacnd  10615  gchaleph2  10675  elwina  10689  elina  10690  winaon  10691  inawina  10693  winainf  10697  winalim  10698  tskr1om2  10771  r1tskina  10785  gruina  10821  grur1a  10822  indpi  10910  nqerrel  10935  recidnq  10968  ltaddnq  10977  pncan3  11483  divcan2  11898  ltp1  12073  ltm1  12075  recreclt  12132  elnn0z  12622  nn0ind-raph  12714  fzdifsuc  13631  2tnp1ge0ge0  13882  fsuppmapnn0fiubex  14048  faclbnd5  14354  hashfun  14494  ccatalpha  14652  caucvgrlem  15750  fsumcnv  15850  fprodcnv  16063  ef01bndlem  16265  sin01gt0  16271  cos01gt0  16272  egt2lt3  16287  cnso  16328  ltoddhalfle  16444  4sqlem12  17041  funcres  17978  fuchom  18046  xpsmnd  18866  xpsgrp  19156  mulgfval  19166  mulgfvalALT  19167  nmznsg  19265  frgp0  19861  gsumval3lem2  20007  gsumval3  20008  xpsrngd  20288  xpsringd  20447  pwssplit1  21217  pzriprnglem4  21671  mvrf1  22172  psdmul  22366  ply1chr  22503  blssioo  24989  dvidlem  26111  dvcj  26146  dvrec  26151  rolle  26186  cmvth  26187  mvth  26188  dvlip  26189  dvlipcn  26190  dv11cn  26197  dvivthlem2  26205  lhop1lem  26209  lhop1  26210  lhop2  26211  q1peqb  26350  pserdv  26629  sinhalfpilem  26665  tangtx  26707  efabl  26752  logi  26789  logneg2  26817  gausslemma2dlem1a  27566  lgseisenlem4  27579  2lgslem3a  27597  2lgslem3b  27598  2lgslem3c  27599  2lgslem3d  27600  dchrisum0lem3  27720  mulogsum  27733  pntrlog2bndlem1  27778  madebday  28130  ltsp1d  28245  pncan3s  28303  divscan2wd  28427  om2noseqoi  28533  n0sge0  28568  bdayfinbndlem1  28697  1reno  28727  prlngsymquadlem  29250  axlowdimlem7  29335  axlowdimlem10  29338  axcontlem6  29356  umgrbi  29488  rusgr1vtxlem  29974  clwwlknonwwlknonb  30494  3wlkond  30559  frcond3  30657  hsn0elch  31637  axpjcl  31789  omlsilem  31791  pjchi  31821  shs00i  31839  chj00i  31876  chabs1  31905  pjspansn  31966  chscllem1  32026  osumcor2i  32033  nonbooli  32040  atcvat4i  32786  xppreima  33027  xdivrec  33283  wrdt2ind  33306  psgndmfi  33449  sqsscirc1  34329  1stmbfm  34682  2ndmbfm  34683  carsgclctunlem2  34741  eulerpartlemgh  34800  hgt750leme  35077  bnj1148  35416  bnj1154  35419  fineqvpow  35552  fineqvacALT  35554  fineqvnttrclse  35561  fineqvr1ombregs  35575  cvmlift3lem5  35836  cvmlift3lem7  35838  currybi  36201  dfon2lem3  36296  dfon2lem7  36300  distel  36314  altopthsn  36474  axtcond  37030  ttc00  37060  bj-ax12  37320  bj-exlimmpbi  37589  irrdiff  38011  rdgssun  38065  wl-ax12v2cl  38193  poimirlem9  38321  poimirlem26  38338  poimirlem27  38339  poimirlem32  38344  dvasin  38396  areacirclem4  38403  heiborlem8  38510  0rngo  38719  dfsuccl4  39164  suceldisj  39508  ax12eq  39756  ax12el  39757  ax12inda  39763  ax12v2-o  39764  nfded  39782  nfded2  39783  nfunidALT2  39784  lshpinN  39804  trlid0  40991  hdmap10lem  42654  lcmineqlem  42860  aks4d1p1p5  42883  fisdomnn  43053  asin1half  43159  renegid  43175  repncan3  43185  sn-00idlem2  43201  reixi  43225  rerecne0d  43258  sn-ltp1  43291  flt4lem7  43432  islssfg2  43839  areaquad  43984  onsupuni  43997  onov0suclim  44042  minregex  44301  wfac8prim  45752  fperdvper  46674  itgvol0  46723  stoweidlem13  46768  stoweidlem26  46781  stoweidlem34  46789  wallispilem4  46823  dirkercncflem1  46858  dirkercncflem3  46860  dirkercncflem4  46861  fourierdlem35  46897  fourierdlem73  46934  funressndmafv2rn  48001  dfatbrafv2b  48023  fnbrafv2b  48026  ichnfimlem  48253  lighneallem4b  48402  nprmdvdsfacm1lem4  48416  sbgoldbwt  48583  sbgoldbalt  48587  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  bgoldbtbndlem1  48611  bgoldbtbndlem3  48613  grimidvtxedg  48691  tposideq  49707  iooii  49737  0thincg  50277  oduoppcciso  50385