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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  dedt  1081  eqcomd  2804  nfabdw  2976  eqvisset  3458  vtocl  3507  vtoclgf  3513  vtoclg1f  3514  vtoclg  3515  eueq3  3650  sbc2or  3729  csbiegf  3861  un00  4350  elimhyp  4488  elimhyp2v  4489  elimhyp3v  4490  elimhyp4v  4491  elimdhyp  4493  keephyp2v  4495  keephyp3v  4496  preq12b  4741  nfopd  4782  ssex  5189  opthwiener  5369  isso2i  5472  nfimad  5905  dfrel2  6013  ordtri3or  6191  on0eqel  6276  funsng  6375  cnvresid  6403  nffvd  6657  fnbrfvb  6693  fvelrnb  6701  fvelimab  6712  funfvop  6797  fvsnun2  6922  rnmptcOLD  6947  iunpw  7473  onsucuni  7523  onuninsuci  7535  tposf12  7900  oaword1  8161  oneo  8190  nnaword1  8238  nnneo  8261  inficl  8873  fipwuni  8874  infeq5i  9083  cantnflt  9119  cantnflem1  9136  cnfcom  9147  rankidn  9235  rankr1id  9275  rankxpsuc  9295  iscard  9388  iscard2  9389  carduni  9394  cardmin2  9412  infxpenlem  9424  alephgeom  9493  cardaleph  9500  infenaleph  9502  iscard3  9504  alephsson  9511  alephfp  9519  alephval3  9521  dfac12k  9558  axdc3lem2  9862  alephval2  9983  alephreg  9993  cfpwsdom  9995  alephom  9996  axrepndlem1  10003  axunndlem1  10006  axunnd  10007  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem2  10014  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  gchaleph2  10083  elwina  10097  elina  10098  winaon  10099  inawina  10101  winainf  10105  winalim  10106  tskr1om2  10179  r1tskina  10193  gruina  10229  grur1a  10230  indpi  10318  nqerrel  10343  recidnq  10376  ltaddnq  10385  pncan3  10883  divcan2  11295  ltp1  11469  ltm1  11471  recreclt  11528  elnn0z  11982  nn0ind-raph  12070  fzdifsuc  12962  2tnp1ge0ge0  13194  fsuppmapnn0fiubex  13355  faclbnd5  13654  hashfun  13794  ccatalpha  13938  caucvgrlem  15021  fsumcnv  15120  fprodcnv  15329  ef01bndlem  15529  sin01gt0  15535  cos01gt0  15536  egt2lt3  15551  cnso  15592  ltoddhalfle  15702  4sqlem12  16282  funcres  17158  fuchom  17223  xpsmnd  17943  xpsgrp  18210  mulgfval  18218  mulgfvalALT  18219  nmznsg  18312  frgp0  18878  gsumval3lem2  19019  gsumval3  19020  pwssplit1  19824  mvrf1  20663  blssioo  23400  dvidlem  24518  dvcj  24553  dvrec  24558  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  dvlipcn  24597  dv11cn  24604  dvivthlem2  24612  lhop1lem  24616  lhop1  24617  lhop2  24618  q1peqb  24755  pserdv  25024  sinhalfpilem  25056  tangtx  25098  efabl  25142  logneg2  25206  gausslemma2dlem1a  25949  lgseisenlem4  25962  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  dchrisum0lem3  26103  mulogsum  26116  pntrlog2bndlem1  26161  axlowdimlem7  26742  axlowdimlem10  26745  axcontlem6  26763  umgrbi  26894  rusgr1vtxlem  27377  clwwlknonwwlknonb  27891  3wlkond  27956  frcond3  28054  hsn0elch  29031  axpjcl  29183  omlsilem  29185  pjchi  29215  shs00i  29233  chj00i  29270  chabs1  29299  pjspansn  29360  chscllem1  29420  osumcor2i  29427  nonbooli  29434  atcvat4i  30180  xppreima  30408  xdivrec  30629  wrdt2ind  30653  psgndmfi  30790  sqsscirc1  31261  1stmbfm  31628  2ndmbfm  31629  carsgclctunlem2  31687  eulerpartlemgh  31746  hgt750leme  32039  bnj1148  32378  bnj1154  32381  cvmlift3lem5  32683  cvmlift3lem7  32685  logi  33079  dfon2lem3  33143  dfon2lem7  33147  distel  33161  altopthsn  33535  bj-ax12  34103  bj-exlimmpbi  34353  irrdiff  34740  rdgssun  34795  poimirlem9  35066  poimirlem26  35083  poimirlem27  35084  poimirlem32  35089  dvasin  35141  areacirclem4  35148  heiborlem8  35256  0rngo  35465  ax12eq  36237  ax12el  36238  ax12inda  36244  ax12v2-o  36245  nfded  36263  nfded2  36264  nfunidALT2  36265  lshpinN  36285  trlid0  37472  hdmap10lem  39135  lcmineqlem  39340  metakunt24  39373  renegid  39511  repncan3  39521  sn-00idlem2  39537  reixi  39559  sn-ltp1  39588  islssfg2  40015  areaquad  40166  fperdvper  42561  itgvol0  42610  stoweidlem13  42655  stoweidlem26  42668  stoweidlem34  42676  wallispilem4  42710  dirkercncflem1  42745  dirkercncflem3  42747  dirkercncflem4  42748  fourierdlem35  42784  fourierdlem73  42821  funressndmafv2rn  43779  dfatbrafv2b  43801  fnbrafv2b  43804  ichnfimlem  43980  lighneallem4b  44127  sbgoldbwt  44295  sbgoldbalt  44299  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  bgoldbtbndlem3  44325