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  1081  eqcomd  2732  nfabdwOLD  2917  eqvisset  3481  vtoclg  3533  vtocl  3537  vtoclOLD  3538  vtoclf  3544  vtoclgf  3549  vtoclg1f  3550  vtoclgOLD  3551  eueq3  3704  sbc2or  3784  csbiegf  3925  un00  4439  elimhyp  4588  elimhyp2v  4589  elimhyp3v  4590  elimhyp4v  4591  elimdhyp  4593  keephyp2v  4595  keephyp3v  4596  preq12b  4849  nfopd  4888  ssex  5318  opthwiener  5512  isso2i  5621  nfimad  6070  dfrel2  6192  ordtri3or  6400  on0eqel  6492  funsng  6602  cnvresid  6630  nffvd  6905  fnbrfvb  6946  fvelrnb  6955  fvelimab  6967  funfvop  7055  fvsnun2  7189  iunpw  7771  onsucuni  7829  onuninsuci  7842  tposf12  8258  oaword1  8574  oneo  8603  nnaword1  8651  nnneo  8677  naddword1  8713  1sdom2dom  9274  inficl  9461  fipwuni  9462  infeq5i  9672  cantnflt  9708  cantnflem1  9725  cnfcom  9736  brttrcl  9749  rankidn  9858  rankr1id  9898  rankxpsuc  9918  iscard  10011  iscard2  10012  carduni  10017  cardmin2  10035  infxpenlem  10049  alephgeom  10118  cardaleph  10125  infenaleph  10127  iscard3  10129  alephsson  10136  alephfp  10144  alephval3  10146  dfac12k  10183  axdc3lem2  10485  alephval2  10606  alephreg  10616  cfpwsdom  10618  alephom  10619  axrepndlem1  10626  axunndlem1  10629  axunnd  10630  axpowndlem2  10632  axpowndlem3  10633  axpowndlem4  10634  axpownd  10635  axregndlem2  10637  axinfndlem1  10639  axinfnd  10640  axacndlem4  10644  axacndlem5  10645  axacnd  10646  gchaleph2  10706  elwina  10720  elina  10721  winaon  10722  inawina  10724  winainf  10728  winalim  10729  tskr1om2  10802  r1tskina  10816  gruina  10852  grur1a  10853  indpi  10941  nqerrel  10966  recidnq  10999  ltaddnq  11008  pncan3  11509  divcan2  11922  ltp1  12099  ltm1  12101  recreclt  12159  elnn0z  12617  nn0ind-raph  12708  fzdifsuc  13609  2tnp1ge0ge0  13843  fsuppmapnn0fiubex  14006  faclbnd5  14310  hashfun  14449  ccatalpha  14596  caucvgrlem  15672  fsumcnv  15772  fprodcnv  15980  ef01bndlem  16181  sin01gt0  16187  cos01gt0  16188  egt2lt3  16203  cnso  16244  ltoddhalfle  16358  4sqlem12  16953  funcres  17910  fuchom  17980  fuchomOLD  17981  xpsmnd  18762  xpsgrp  19049  mulgfval  19059  mulgfvalALT  19060  nmznsg  19158  frgp0  19754  gsumval3lem2  19900  gsumval3  19901  xpsrngd  20158  xpsringd  20307  pwssplit1  21033  pzriprnglem4  21470  mvrf1  21991  psdmul  22156  ply1chr  22294  blssioo  24799  dvidlem  25932  dvcj  25970  dvrec  25975  rolle  26010  cmvth  26011  cmvthOLD  26012  mvth  26013  dvlip  26014  dvlipcn  26015  dv11cn  26022  dvivthlem2  26030  lhop1lem  26034  lhop1  26035  lhop2  26036  q1peqb  26180  pserdv  26456  sinhalfpilem  26488  tangtx  26530  efabl  26574  logi  26611  logneg2  26639  gausslemma2dlem1a  27391  lgseisenlem4  27404  2lgslem3a  27422  2lgslem3b  27423  2lgslem3c  27424  2lgslem3d  27425  dchrisum0lem3  27545  mulogsum  27558  pntrlog2bndlem1  27603  madebday  27920  pncan3s  28077  divscan2wd  28194  om2noseqlt  28270  om2noseqoi  28274  n0sge0  28306  axlowdimlem7  28879  axlowdimlem10  28882  axcontlem6  28900  umgrbi  29034  rusgr1vtxlem  29521  clwwlknonwwlknonb  30036  3wlkond  30101  frcond3  30199  hsn0elch  31178  axpjcl  31330  omlsilem  31332  pjchi  31362  shs00i  31380  chj00i  31417  chabs1  31446  pjspansn  31507  chscllem1  31567  osumcor2i  31574  nonbooli  31581  atcvat4i  32327  xppreima  32563  xdivrec  32791  wrdt2ind  32820  psgndmfi  32980  sqsscirc1  33736  1stmbfm  34107  2ndmbfm  34108  carsgclctunlem2  34166  eulerpartlemgh  34225  hgt750leme  34517  bnj1148  34854  bnj1154  34857  fineqvpow  34945  fineqvacALT  34947  cvmlift3lem5  35164  cvmlift3lem7  35166  currybi  35529  dfon2lem3  35622  dfon2lem7  35626  distel  35640  altopthsn  35798  bj-ax12  36374  bj-exlimmpbi  36632  irrdiff  37046  rdgssun  37098  poimirlem9  37343  poimirlem26  37360  poimirlem27  37361  poimirlem32  37366  dvasin  37418  areacirclem4  37425  heiborlem8  37532  0rngo  37741  ax12eq  38652  ax12el  38653  ax12inda  38659  ax12v2-o  38660  nfded  38678  nfded2  38679  nfunidALT2  38680  lshpinN  38700  trlid0  39888  hdmap10lem  41551  lcmineqlem  41764  aks4d1p1p5  41787  metakunt24  41936  fisdomnn  41990  renegid  42084  repncan3  42094  sn-00idlem2  42110  reixi  42133  sn-ltp1  42175  flt4lem7  42349  islssfg2  42769  areaquad  42918  onsupuni  42931  onov0suclim  42977  minregex  43238  fperdvper  45576  itgvol0  45625  stoweidlem13  45670  stoweidlem26  45683  stoweidlem34  45691  wallispilem4  45725  dirkercncflem1  45760  dirkercncflem3  45762  dirkercncflem4  45763  fourierdlem35  45799  fourierdlem73  45836  funressndmafv2rn  46872  dfatbrafv2b  46894  fnbrafv2b  46897  ichnfimlem  47071  lighneallem4b  47217  sbgoldbwt  47385  sbgoldbalt  47389  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  bgoldbtbndlem1  47413  bgoldbtbndlem3  47415  grimidvtxedg  47491  iooii  48287  0thincg  48407