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  27395  pncan3s  27544  divscan2wd  27647  axlowdimlem7  28237  axlowdimlem10  28240  axcontlem6  28258  umgrbi  28392  rusgr1vtxlem  28875  clwwlknonwwlknonb  29390  3wlkond  29455  frcond3  29553  hsn0elch  30532  axpjcl  30684  omlsilem  30686  pjchi  30716  shs00i  30734  chj00i  30771  chabs1  30800  pjspansn  30861  chscllem1  30921  osumcor2i  30928  nonbooli  30935  atcvat4i  31681  xppreima  31902  xdivrec  32124  wrdt2ind  32148  psgndmfi  32288  ply1chr  32692  sqsscirc1  32919  1stmbfm  33290  2ndmbfm  33291  carsgclctunlem2  33349  eulerpartlemgh  33408  hgt750leme  33701  bnj1148  34038  bnj1154  34041  fineqvpow  34127  fineqvacALT  34129  cvmlift3lem5  34345  cvmlift3lem7  34347  currybi  34700  logi  34735  dfon2lem3  34788  dfon2lem7  34792  distel  34806  altopthsn  34964  gg-cmvth  35212  bj-ax12  35582  bj-exlimmpbi  35841  irrdiff  36255  rdgssun  36307  poimirlem9  36545  poimirlem26  36562  poimirlem27  36563  poimirlem32  36568  dvasin  36620  areacirclem4  36627  heiborlem8  36734  0rngo  36943  ax12eq  37859  ax12el  37860  ax12inda  37866  ax12v2-o  37867  nfded  37885  nfded2  37886  nfunidALT2  37887  lshpinN  37907  trlid0  39095  hdmap10lem  40758  lcmineqlem  40965  aks4d1p1p5  40988  metakunt24  41056  renegid  41294  repncan3  41304  sn-00idlem2  41320  reixi  41343  sn-ltp1  41384  flt4lem7  41449  islssfg2  41861  areaquad  42013  onsupuni  42026  onov0suclim  42072  minregex  42333  fperdvper  44683  itgvol0  44732  stoweidlem13  44777  stoweidlem26  44790  stoweidlem34  44798  wallispilem4  44832  dirkercncflem1  44867  dirkercncflem3  44869  dirkercncflem4  44870  fourierdlem35  44906  fourierdlem73  44943  funressndmafv2rn  45979  dfatbrafv2b  46001  fnbrafv2b  46004  ichnfimlem  46179  lighneallem4b  46325  sbgoldbwt  46493  sbgoldbalt  46497  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  bgoldbtbndlem1  46521  bgoldbtbndlem3  46523  xpsrngd  46728  pzriprnglem4  46856  iooii  47598  0thincg  47718