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  1085  eqcomd  2739  nfabdwOLD  2928  eqvisset  3492  vtoclf  3548  vtocl  3550  vtoclgf  3555  vtoclg1f  3556  vtoclg  3557  vtoclgOLD  3558  eueq3  3708  sbc2or  3787  csbiegf  3928  un00  4443  elimhyp  4594  elimhyp2v  4595  elimhyp3v  4596  elimhyp4v  4597  elimdhyp  4599  keephyp2v  4601  keephyp3v  4602  preq12b  4852  nfopd  4891  ssex  5322  opthwiener  5515  isso2i  5624  nfimad  6069  dfrel2  6189  ordtri3or  6397  on0eqel  6489  funsng  6600  cnvresid  6628  nffvd  6904  fnbrfvb  6945  fvelrnb  6953  fvelimab  6965  funfvop  7052  fvsnun2  7181  rnmptcOLD  7209  iunpw  7758  onsucuni  7816  onuninsuci  7829  tposf12  8236  oaword1  8552  oneo  8581  nnaword1  8629  nnneo  8654  naddword1  8690  1sdom2dom  9247  inficl  9420  fipwuni  9421  infeq5i  9631  cantnflt  9667  cantnflem1  9684  cnfcom  9695  brttrcl  9708  rankidn  9817  rankr1id  9857  rankxpsuc  9877  iscard  9970  iscard2  9971  carduni  9976  cardmin2  9994  infxpenlem  10008  alephgeom  10077  cardaleph  10084  infenaleph  10086  iscard3  10088  alephsson  10095  alephfp  10103  alephval3  10105  dfac12k  10142  axdc3lem2  10446  alephval2  10567  alephreg  10577  cfpwsdom  10579  alephom  10580  axrepndlem1  10587  axunndlem1  10590  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axpownd  10596  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607  gchaleph2  10667  elwina  10681  elina  10682  winaon  10683  inawina  10685  winainf  10689  winalim  10690  tskr1om2  10763  r1tskina  10777  gruina  10813  grur1a  10814  indpi  10902  nqerrel  10927  recidnq  10960  ltaddnq  10969  pncan3  11468  divcan2  11880  ltp1  12054  ltm1  12056  recreclt  12113  elnn0z  12571  nn0ind-raph  12662  fzdifsuc  13561  2tnp1ge0ge0  13794  fsuppmapnn0fiubex  13957  faclbnd5  14258  hashfun  14397  ccatalpha  14543  caucvgrlem  15619  fsumcnv  15719  fprodcnv  15927  ef01bndlem  16127  sin01gt0  16133  cos01gt0  16134  egt2lt3  16149  cnso  16190  ltoddhalfle  16304  4sqlem12  16889  funcres  17846  fuchom  17913  fuchomOLD  17914  xpsmnd  18665  xpsgrp  18942  mulgfval  18952  mulgfvalALT  18953  nmznsg  19048  frgp0  19628  gsumval3lem2  19774  gsumval3  19775  xpsringd  20145  pwssplit1  20670  mvrf1  21545  blssioo  24311  dvidlem  25432  dvcj  25467  dvrec  25472  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvlipcn  25511  dv11cn  25518  dvivthlem2  25526  lhop1lem  25530  lhop1  25531  lhop2  25532  q1peqb  25672  pserdv  25941  sinhalfpilem  25973  tangtx  26015  efabl  26059  logneg2  26123  gausslemma2dlem1a  26868  lgseisenlem4  26881  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  dchrisum0lem3  27022  mulogsum  27035  pntrlog2bndlem1  27080  madebday  27394  pncan3s  27541  divscan2wd  27644  axlowdimlem7  28206  axlowdimlem10  28209  axcontlem6  28227  umgrbi  28361  rusgr1vtxlem  28844  clwwlknonwwlknonb  29359  3wlkond  29424  frcond3  29522  hsn0elch  30501  axpjcl  30653  omlsilem  30655  pjchi  30685  shs00i  30703  chj00i  30740  chabs1  30769  pjspansn  30830  chscllem1  30890  osumcor2i  30897  nonbooli  30904  atcvat4i  31650  xppreima  31871  xdivrec  32093  wrdt2ind  32117  psgndmfi  32257  ply1chr  32661  sqsscirc1  32888  1stmbfm  33259  2ndmbfm  33260  carsgclctunlem2  33318  eulerpartlemgh  33377  hgt750leme  33670  bnj1148  34007  bnj1154  34010  fineqvpow  34096  fineqvacALT  34098  cvmlift3lem5  34314  cvmlift3lem7  34316  currybi  34669  logi  34704  dfon2lem3  34757  dfon2lem7  34761  distel  34775  altopthsn  34933  gg-cmvth  35181  bj-ax12  35534  bj-exlimmpbi  35793  irrdiff  36207  rdgssun  36259  poimirlem9  36497  poimirlem26  36514  poimirlem27  36515  poimirlem32  36520  dvasin  36572  areacirclem4  36579  heiborlem8  36686  0rngo  36895  ax12eq  37811  ax12el  37812  ax12inda  37818  ax12v2-o  37819  nfded  37837  nfded2  37838  nfunidALT2  37839  lshpinN  37859  trlid0  39047  hdmap10lem  40710  lcmineqlem  40917  aks4d1p1p5  40940  metakunt24  41008  renegid  41246  repncan3  41256  sn-00idlem2  41272  reixi  41295  sn-ltp1  41336  flt4lem7  41401  islssfg2  41813  areaquad  41965  onsupuni  41978  onov0suclim  42024  minregex  42285  fperdvper  44635  itgvol0  44684  stoweidlem13  44729  stoweidlem26  44742  stoweidlem34  44750  wallispilem4  44784  dirkercncflem1  44819  dirkercncflem3  44821  dirkercncflem4  44822  fourierdlem35  44858  fourierdlem73  44895  funressndmafv2rn  45931  dfatbrafv2b  45953  fnbrafv2b  45956  ichnfimlem  46131  lighneallem4b  46277  sbgoldbwt  46445  sbgoldbalt  46449  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbndlem1  46473  bgoldbtbndlem3  46475  xpsrngd  46680  pzriprnglem4  46808  iooii  47550  0thincg  47670