Theorem mpbii 233

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  dedt  1083  eqcomd  2740  eqvisset  3497  vtoclg  3553  vtocl  3557  vtoclOLD  3558  vtoclf  3563  vtoclgf  3568  vtoclg1f  3569  vtoclgOLD  3570  eueq3  3719  sbc2or  3799  csbiegf  3941  un00  4450  elimhyp  4595  elimhyp2v  4596  elimhyp3v  4597  elimhyp4v  4598  elimdhyp  4600  keephyp2v  4602  keephyp3v  4603  preq12b  4854  nfopd  4894  ssex  5326  opthwiener  5523  isso2i  5632  nfimad  6088  dfrel2  6210  ordtri3or  6417  on0eqel  6509  funsng  6618  cnvresid  6646  nffvd  6918  fnbrfvb  6959  fvelrnb  6968  fvelimab  6980  funfvop  7069  fvsnun2  7202  iunpw  7789  onsucuni  7847  onuninsuci  7860  tposf12  8274  oaword1  8588  oneo  8617  nnaword1  8665  nnneo  8691  naddword1  8727  1sdom2dom  9280  inficl  9462  fipwuni  9463  infeq5i  9673  cantnflt  9709  cantnflem1  9726  cnfcom  9737  brttrcl  9750  rankidn  9859  rankr1id  9899  rankxpsuc  9919  iscard  10012  iscard2  10013  carduni  10018  cardmin2  10036  infxpenlem  10050  alephgeom  10119  cardaleph  10126  infenaleph  10128  iscard3  10130  alephsson  10137  alephfp  10145  alephval3  10147  dfac12k  10185  axdc3lem2  10488  alephval2  10609  alephreg  10619  cfpwsdom  10621  alephom  10622  axrepndlem1  10629  axunndlem1  10632  axunnd  10633  axpowndlem2  10635  axpowndlem3  10636  axpowndlem4  10637  axpownd  10638  axregndlem2  10640  axinfndlem1  10642  axinfnd  10643  axacndlem4  10647  axacndlem5  10648  axacnd  10649  gchaleph2  10709  elwina  10723  elina  10724  winaon  10725  inawina  10727  winainf  10731  winalim  10732  tskr1om2  10805  r1tskina  10819  gruina  10855  grur1a  10856  indpi  10944  nqerrel  10969  recidnq  11002  ltaddnq  11011  pncan3  11513  divcan2  11927  ltp1  12104  ltm1  12106  recreclt  12164  elnn0z  12623  nn0ind-raph  12715  fzdifsuc  13620  2tnp1ge0ge0  13865  fsuppmapnn0fiubex  14029  faclbnd5  14333  hashfun  14472  ccatalpha  14627  caucvgrlem  15705  fsumcnv  15805  fprodcnv  16015  ef01bndlem  16216  sin01gt0  16222  cos01gt0  16223  egt2lt3  16238  cnso  16279  ltoddhalfle  16394  4sqlem12  16989  funcres  17946  fuchom  18016  fuchomOLD  18017  xpsmnd  18802  xpsgrp  19089  mulgfval  19099  mulgfvalALT  19100  nmznsg  19198  frgp0  19792  gsumval3lem2  19938  gsumval3  19939  xpsrngd  20196  xpsringd  20345  pwssplit1  21075  pzriprnglem4  21512  mvrf1  22023  psdmul  22187  ply1chr  22325  blssioo  24830  dvidlem  25964  dvcj  26002  dvrec  26007  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlipcn  26047  dv11cn  26054  dvivthlem2  26062  lhop1lem  26066  lhop1  26067  lhop2  26068  q1peqb  26209  pserdv  26487  sinhalfpilem  26519  tangtx  26561  efabl  26606  logi  26643  logneg2  26671  gausslemma2dlem1a  27423  lgseisenlem4  27436  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  dchrisum0lem3  27577  mulogsum  27590  pntrlog2bndlem1  27635  madebday  27952  sltp1d  28062  pncan3s  28117  divscan2wd  28236  om2noseqlt  28319  om2noseqoi  28323  n0sge0  28355  axlowdimlem7  28977  axlowdimlem10  28980  axcontlem6  28998  umgrbi  29132  rusgr1vtxlem  29619  clwwlknonwwlknonb  30134  3wlkond  30199  frcond3  30297  hsn0elch  31276  axpjcl  31428  omlsilem  31430  pjchi  31460  shs00i  31478  chj00i  31515  chabs1  31544  pjspansn  31605  chscllem1  31665  osumcor2i  31672  nonbooli  31679  atcvat4i  32425  xppreima  32661  xdivrec  32893  wrdt2ind  32922  psgndmfi  33100  sqsscirc1  33868  1stmbfm  34241  2ndmbfm  34242  carsgclctunlem2  34300  eulerpartlemgh  34359  hgt750leme  34651  bnj1148  34988  bnj1154  34991  fineqvpow  35088  fineqvacALT  35090  cvmlift3lem5  35307  cvmlift3lem7  35309  currybi  35672  dfon2lem3  35766  dfon2lem7  35770  distel  35784  altopthsn  35942  bj-ax12  36639  bj-exlimmpbi  36895  irrdiff  37308  rdgssun  37360  wl-ax12v2cl  37486  poimirlem9  37615  poimirlem26  37632  poimirlem27  37633  poimirlem32  37638  dvasin  37690  areacirclem4  37697  heiborlem8  37804  0rngo  38013  ax12eq  38922  ax12el  38923  ax12inda  38929  ax12v2-o  38930  nfded  38948  nfded2  38949  nfunidALT2  38950  lshpinN  38970  trlid0  40158  hdmap10lem  41821  lcmineqlem  42033  aks4d1p1p5  42056  metakunt24  42209  fisdomnn  42263  asin1half  42365  renegid  42379  repncan3  42389  sn-00idlem2  42405  reixi  42428  sn-ltp1  42470  flt4lem7  42645  islssfg2  43059  areaquad  43204  onsupuni  43217  onov0suclim  43263  minregex  43523  fperdvper  45874  itgvol0  45923  stoweidlem13  45968  stoweidlem26  45981  stoweidlem34  45989  wallispilem4  46023  dirkercncflem1  46058  dirkercncflem3  46060  dirkercncflem4  46061  fourierdlem35  46097  fourierdlem73  46134  funressndmafv2rn  47172  dfatbrafv2b  47194  fnbrafv2b  47197  ichnfimlem  47387  lighneallem4b  47533  sbgoldbwt  47701  sbgoldbalt  47705  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem1  47729  bgoldbtbndlem3  47731  grimidvtxedg  47813  iooii  48713  0thincg  48850  oduoppcciso  48881