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  2739  eqvisset  3457  vtoclg  3508  vtocl  3512  vtoclOLD  3513  vtoclf  3518  vtoclgf  3522  vtoclg1f  3523  eueq3  3666  sbc2or  3746  csbiegf  3879  un00  4394  elimhyp  4540  elimhyp2v  4541  elimhyp3v  4542  elimhyp4v  4543  elimdhyp  4545  keephyp2v  4547  keephyp3v  4548  preq12b  4801  nfopd  4841  ssex  5261  opthwiener  5457  isso2i  5564  nfimad  6022  dfrel2  6141  ordtri3or  6343  on0eqel  6436  funsng  6537  cnvresid  6565  nffvd  6840  fnbrfvb  6878  fvelrnb  6888  fvelimab  6900  funfvop  6989  fvsnun2  7123  iunpw  7710  onsucuni  7764  onuninsuci  7776  tposf12  8187  oaword1  8473  oneo  8502  nnaword1  8550  nnneo  8576  naddword1  8612  1sdom2dom  9145  inficl  9316  fipwuni  9317  infeq5i  9533  cantnflt  9569  cantnflem1  9586  cnfcom  9597  brttrcl  9610  rankidn  9722  rankr1id  9762  rankxpsuc  9782  iscard  9875  iscard2  9876  carduni  9881  cardmin2  9899  infxpenlem  9911  alephgeom  9980  cardaleph  9987  infenaleph  9989  iscard3  9991  alephsson  9998  alephfp  10006  alephval3  10008  dfac12k  10046  axdc3lem2  10349  alephval2  10470  alephreg  10480  cfpwsdom  10482  alephom  10483  axrepndlem1  10490  axunndlem1  10493  axunnd  10494  axpowndlem2  10496  axpowndlem3  10497  axpowndlem4  10498  axpownd  10499  axregndlem2  10501  axinfndlem1  10503  axinfnd  10504  axacndlem4  10508  axacndlem5  10509  axacnd  10510  gchaleph2  10570  elwina  10584  elina  10585  winaon  10586  inawina  10588  winainf  10592  winalim  10593  tskr1om2  10666  r1tskina  10680  gruina  10716  grur1a  10717  indpi  10805  nqerrel  10830  recidnq  10863  ltaddnq  10872  pncan3  11375  divcan2  11791  ltp1  11968  ltm1  11970  recreclt  12028  elnn0z  12488  nn0ind-raph  12579  fzdifsuc  13486  2tnp1ge0ge0  13735  fsuppmapnn0fiubex  13901  faclbnd5  14207  hashfun  14346  ccatalpha  14503  caucvgrlem  15582  fsumcnv  15682  fprodcnv  15892  ef01bndlem  16095  sin01gt0  16101  cos01gt0  16102  egt2lt3  16117  cnso  16158  ltoddhalfle  16274  4sqlem12  16870  funcres  17805  fuchom  17873  xpsmnd  18687  xpsgrp  18974  mulgfval  18984  mulgfvalALT  18985  nmznsg  19082  frgp0  19674  gsumval3lem2  19820  gsumval3  19821  xpsrngd  20099  xpsringd  20252  pwssplit1  20995  pzriprnglem4  21423  mvrf1  21924  psdmul  22082  ply1chr  22222  blssioo  24711  dvidlem  25844  dvcj  25882  dvrec  25887  rolle  25922  cmvth  25923  cmvthOLD  25924  mvth  25925  dvlip  25926  dvlipcn  25927  dv11cn  25934  dvivthlem2  25942  lhop1lem  25946  lhop1  25947  lhop2  25948  q1peqb  26089  pserdv  26367  sinhalfpilem  26400  tangtx  26442  efabl  26487  logi  26524  logneg2  26552  gausslemma2dlem1a  27304  lgseisenlem4  27317  2lgslem3a  27335  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  dchrisum0lem3  27458  mulogsum  27471  pntrlog2bndlem1  27516  madebday  27846  sltp1d  27959  pncan3s  28014  divscan2wd  28137  om2noseqoi  28234  n0sge0  28267  axlowdimlem7  28928  axlowdimlem10  28931  axcontlem6  28949  umgrbi  29081  rusgr1vtxlem  29568  clwwlknonwwlknonb  30088  3wlkond  30153  frcond3  30251  hsn0elch  31230  axpjcl  31382  omlsilem  31384  pjchi  31414  shs00i  31432  chj00i  31469  chabs1  31498  pjspansn  31559  chscllem1  31619  osumcor2i  31626  nonbooli  31633  atcvat4i  32379  xppreima  32629  xdivrec  32914  wrdt2ind  32941  psgndmfi  33074  sqsscirc1  33942  1stmbfm  34294  2ndmbfm  34295  carsgclctunlem2  34353  eulerpartlemgh  34412  hgt750leme  34692  bnj1148  35029  bnj1154  35032  fineqvr1ombregs  35156  fineqvpow  35159  fineqvacALT  35161  fineqvnttrclse  35165  cvmlift3lem5  35388  cvmlift3lem7  35390  currybi  35753  dfon2lem3  35848  dfon2lem7  35852  distel  35866  altopthsn  36026  bj-ax12  36722  bj-exlimmpbi  36978  irrdiff  37391  rdgssun  37443  wl-ax12v2cl  37571  poimirlem9  37689  poimirlem26  37706  poimirlem27  37707  poimirlem32  37712  dvasin  37764  areacirclem4  37771  heiborlem8  37878  0rngo  38087  dfsuccl4  38507  ax12eq  39060  ax12el  39061  ax12inda  39067  ax12v2-o  39068  nfded  39086  nfded2  39087  nfunidALT2  39088  lshpinN  39108  trlid0  40295  hdmap10lem  41958  lcmineqlem  42165  aks4d1p1p5  42188  fisdomnn  42362  asin1half  42475  renegid  42491  repncan3  42501  sn-00idlem2  42517  reixi  42541  sn-ltp1  42594  flt4lem7  42777  islssfg2  43188  areaquad  43333  onsupuni  43346  onov0suclim  43391  minregex  43651  wfac8prim  45119  fperdvper  46041  itgvol0  46090  stoweidlem13  46135  stoweidlem26  46148  stoweidlem34  46156  wallispilem4  46190  dirkercncflem1  46225  dirkercncflem3  46227  dirkercncflem4  46228  fourierdlem35  46264  fourierdlem73  46301  funressndmafv2rn  47347  dfatbrafv2b  47369  fnbrafv2b  47372  ichnfimlem  47587  lighneallem4b  47733  sbgoldbwt  47901  sbgoldbalt  47905  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  bgoldbtbndlem1  47929  bgoldbtbndlem3  47931  grimidvtxedg  48009  tposideq  49012  iooii  49042  0thincg  49583  oduoppcciso  49691