Theorem mpbii 235

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  elimhOLD  1077  dedt  1078  eqcomd  2827  nfabdw  3000  eqvisset  3511  vtocl  3559  vtoclgf  3565  vtoclg1f  3566  vtoclg  3567  eueq3  3702  sbc2or  3781  csbiegf  3916  un00  4394  elimhyp  4530  elimhyp2v  4531  elimhyp3v  4532  elimhyp4v  4533  elimdhyp  4535  keephyp2v  4537  keephyp3v  4538  preq12b  4781  nfopd  4820  ssex  5225  opthwiener  5404  isso2i  5508  nfimad  5938  dfrel2  6046  ordtri3or  6223  on0eqel  6308  funsng  6405  cnvresid  6433  nffvd  6682  fnbrfvb  6718  fvelrnb  6726  fvelimab  6737  funfvop  6820  fvsnun2  6945  rnmptcOLD  6970  iunpw  7493  onsucuni  7543  onuninsuci  7555  tposf12  7917  oaword1  8178  oneo  8207  nnaword1  8255  nnneo  8278  inficl  8889  fipwuni  8890  infeq5i  9099  cantnflt  9135  cantnflem1  9152  cnfcom  9163  rankidn  9251  rankr1id  9291  rankxpsuc  9311  iscard  9404  iscard2  9405  carduni  9410  cardmin2  9427  infxpenlem  9439  alephgeom  9508  cardaleph  9515  infenaleph  9517  iscard3  9519  alephsson  9526  alephfp  9534  alephval3  9536  dfac12k  9573  axdc3lem2  9873  alephval2  9994  alephreg  10004  cfpwsdom  10006  alephom  10007  axrepndlem1  10014  axunndlem1  10017  axunnd  10018  axpowndlem2  10020  axpowndlem3  10021  axpowndlem4  10022  axpownd  10023  axregndlem2  10025  axinfndlem1  10027  axinfnd  10028  axacndlem4  10032  axacndlem5  10033  axacnd  10034  gchaleph2  10094  elwina  10108  elina  10109  winaon  10110  inawina  10112  winainf  10116  winalim  10117  tskr1om2  10190  r1tskina  10204  gruina  10240  grur1a  10241  indpi  10329  nqerrel  10354  recidnq  10387  ltaddnq  10396  pncan3  10894  divcan2  11306  ltp1  11480  ltm1  11482  recreclt  11539  elnn0z  11995  nn0ind-raph  12083  fzdifsuc  12968  2tnp1ge0ge0  13200  fsuppmapnn0fiubex  13361  faclbnd5  13659  hashfun  13799  ccatalpha  13947  caucvgrlem  15029  fsumcnv  15128  fprodcnv  15337  ef01bndlem  15537  sin01gt0  15543  cos01gt0  15544  egt2lt3  15559  cnso  15600  ltoddhalfle  15710  4sqlem12  16292  funcres  17166  fuchom  17231  xpsmnd  17951  xpsgrp  18218  mulgfval  18226  mulgfvalALT  18227  nmznsg  18320  frgp0  18886  gsumval3lem2  19026  gsumval3  19027  pwssplit1  19831  mvrf1  20205  blssioo  23403  dvidlem  24513  dvcj  24547  dvrec  24552  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlipcn  24591  dv11cn  24598  dvivthlem2  24606  lhop1lem  24610  lhop1  24611  lhop2  24612  q1peqb  24748  pserdv  25017  sinhalfpilem  25049  tangtx  25091  efabl  25134  logneg2  25198  gausslemma2dlem1a  25941  lgseisenlem4  25954  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  dchrisum0lem3  26095  mulogsum  26108  pntrlog2bndlem1  26153  axlowdimlem7  26734  axlowdimlem10  26737  axcontlem6  26755  umgrbi  26886  rusgr1vtxlem  27369  clwwlknonwwlknonb  27885  3wlkond  27950  frcond3  28048  hsn0elch  29025  axpjcl  29177  omlsilem  29179  pjchi  29209  shs00i  29227  chj00i  29264  chabs1  29293  pjspansn  29354  chscllem1  29414  osumcor2i  29421  nonbooli  29428  atcvat4i  30174  xppreima  30394  xdivrec  30603  wrdt2ind  30627  psgndmfi  30740  sqsscirc1  31151  1stmbfm  31518  2ndmbfm  31519  carsgclctunlem2  31577  eulerpartlemgh  31636  hgt750leme  31929  bnj1148  32268  bnj1154  32271  cvmlift3lem5  32570  cvmlift3lem7  32572  logi  32966  dfon2lem3  33030  dfon2lem7  33034  distel  33048  altopthsn  33422  bj-ax12  33990  bj-exlimmpbi  34232  rdgssun  34662  poimirlem9  34916  poimirlem26  34933  poimirlem27  34934  poimirlem32  34939  dvasin  34993  areacirclem4  35000  heiborlem8  35111  0rngo  35320  ax12eq  36092  ax12el  36093  ax12inda  36099  ax12v2-o  36100  nfded  36118  nfded2  36119  nfunidALT2  36120  lshpinN  36140  trlid0  37327  hdmap10lem  38990  renegid  39223  repncan3  39233  sn-00idlem2  39249  sn-ltp1  39267  islssfg2  39691  areaquad  39843  fperdvper  42223  itgvol0  42273  stoweidlem13  42318  stoweidlem26  42331  stoweidlem34  42339  wallispilem4  42373  dirkercncflem1  42408  dirkercncflem3  42410  dirkercncflem4  42411  fourierdlem35  42447  fourierdlem73  42484  funressndmafv2rn  43442  dfatbrafv2b  43464  fnbrafv2b  43467  ichnfimlem2  43642  lighneallem4b  43794  sbgoldbwt  43962  sbgoldbalt  43966  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  bgoldbtbndlem1  43990  bgoldbtbndlem3  43992