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  1084  eqcomd  2742  clelab  2881  nfabdwOLD  2929  eqvisset  3454  vtocl  3503  vtoclgf  3508  vtoclg1f  3509  vtoclg  3510  eueq3  3651  sbc2or  3730  csbiegf  3871  un00  4382  elimhyp  4530  elimhyp2v  4531  elimhyp3v  4532  elimhyp4v  4533  elimdhyp  4535  keephyp2v  4537  keephyp3v  4538  preq12b  4787  nfopd  4826  ssex  5254  opthwiener  5441  isso2i  5549  nfimad  5988  dfrel2  6107  ordtri3or  6313  on0eqel  6403  funsng  6514  cnvresid  6542  nffvd  6816  fnbrfvb  6854  fvelrnb  6862  fvelimab  6873  funfvop  6959  fvsnun2  7087  rnmptcOLD  7115  iunpw  7653  onsucuni  7707  onuninsuci  7719  tposf12  8098  oaword1  8414  oneo  8443  nnaword1  8491  nnneo  8516  1sdom2dom  9068  inficl  9228  fipwuni  9229  infeq5i  9438  cantnflt  9474  cantnflem1  9491  cnfcom  9502  brttrcl  9515  rankidn  9624  rankr1id  9664  rankxpsuc  9684  iscard  9777  iscard2  9778  carduni  9783  cardmin2  9801  infxpenlem  9815  alephgeom  9884  cardaleph  9891  infenaleph  9893  iscard3  9895  alephsson  9902  alephfp  9910  alephval3  9912  dfac12k  9949  axdc3lem2  10253  alephval2  10374  alephreg  10384  cfpwsdom  10386  alephom  10387  axrepndlem1  10394  axunndlem1  10397  axunnd  10398  axpowndlem2  10400  axpowndlem3  10401  axpowndlem4  10402  axpownd  10403  axregndlem2  10405  axinfndlem1  10407  axinfnd  10408  axacndlem4  10412  axacndlem5  10413  axacnd  10414  gchaleph2  10474  elwina  10488  elina  10489  winaon  10490  inawina  10492  winainf  10496  winalim  10497  tskr1om2  10570  r1tskina  10584  gruina  10620  grur1a  10621  indpi  10709  nqerrel  10734  recidnq  10767  ltaddnq  10776  pncan3  11275  divcan2  11687  ltp1  11861  ltm1  11863  recreclt  11920  elnn0z  12378  nn0ind-raph  12466  fzdifsuc  13362  2tnp1ge0ge0  13595  fsuppmapnn0fiubex  13758  faclbnd5  14058  hashfun  14197  ccatalpha  14343  caucvgrlem  15429  fsumcnv  15530  fprodcnv  15738  ef01bndlem  15938  sin01gt0  15944  cos01gt0  15945  egt2lt3  15960  cnso  16001  ltoddhalfle  16115  4sqlem12  16702  funcres  17656  fuchom  17723  fuchomOLD  17724  xpsmnd  18470  xpsgrp  18739  mulgfval  18747  mulgfvalALT  18748  nmznsg  18841  frgp0  19411  gsumval3lem2  19552  gsumval3  19553  pwssplit1  20366  mvrf1  21239  blssioo  24003  dvidlem  25124  dvcj  25159  dvrec  25164  rolle  25199  cmvth  25200  mvth  25201  dvlip  25202  dvlipcn  25203  dv11cn  25210  dvivthlem2  25218  lhop1lem  25222  lhop1  25223  lhop2  25224  q1peqb  25364  pserdv  25633  sinhalfpilem  25665  tangtx  25707  efabl  25751  logneg2  25815  gausslemma2dlem1a  26558  lgseisenlem4  26571  2lgslem3a  26589  2lgslem3b  26590  2lgslem3c  26591  2lgslem3d  26592  dchrisum0lem3  26712  mulogsum  26725  pntrlog2bndlem1  26770  axlowdimlem7  27361  axlowdimlem10  27364  axcontlem6  27382  umgrbi  27516  rusgr1vtxlem  27999  clwwlknonwwlknonb  28515  3wlkond  28580  frcond3  28678  hsn0elch  29655  axpjcl  29807  omlsilem  29809  pjchi  29839  shs00i  29857  chj00i  29894  chabs1  29923  pjspansn  29984  chscllem1  30044  osumcor2i  30051  nonbooli  30058  atcvat4i  30804  xppreima  31028  xdivrec  31246  wrdt2ind  31270  psgndmfi  31410  ply1chr  31714  sqsscirc1  31903  1stmbfm  32272  2ndmbfm  32273  carsgclctunlem2  32331  eulerpartlemgh  32390  hgt750leme  32683  bnj1148  33021  bnj1154  33024  fineqvpow  33110  fineqvacALT  33112  cvmlift3lem5  33330  cvmlift3lem7  33332  logi  33745  dfon2lem3  33806  dfon2lem7  33810  distel  33824  madebday  34125  altopthsn  34308  bj-ax12  34883  bj-exlimmpbi  35142  irrdiff  35541  rdgssun  35593  poimirlem9  35830  poimirlem26  35847  poimirlem27  35848  poimirlem32  35853  dvasin  35905  areacirclem4  35912  heiborlem8  36020  0rngo  36229  ax12eq  36997  ax12el  36998  ax12inda  37004  ax12v2-o  37005  nfded  37023  nfded2  37024  nfunidALT2  37025  lshpinN  37045  trlid0  38232  hdmap10lem  39895  lcmineqlem  40102  aks4d1p1p5  40125  metakunt24  40190  renegid  40393  repncan3  40403  sn-00idlem2  40419  reixi  40441  sn-ltp1  40470  flt4lem7  40533  islssfg2  40934  areaquad  41085  minregex  41179  fperdvper  43509  itgvol0  43558  stoweidlem13  43603  stoweidlem26  43616  stoweidlem34  43624  wallispilem4  43658  dirkercncflem1  43693  dirkercncflem3  43695  dirkercncflem4  43696  fourierdlem35  43732  fourierdlem73  43769  funressndmafv2rn  44773  dfatbrafv2b  44795  fnbrafv2b  44798  ichnfimlem  44973  lighneallem4b  45119  sbgoldbwt  45287  sbgoldbalt  45291  nnsum4primeseven  45310  nnsum4primesevenALTV  45311  bgoldbtbndlem1  45315  bgoldbtbndlem3  45317  iooii  46269  0thincg  46389