Theorem mpbii 234

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  dedt  1089  eqcomd  2746  eqvisset  3452  vtoclg  3502  vtocl  3506  vtoclOLD  3507  vtoclf  3512  vtoclgf  3516  vtoclg1f  3517  eueq3  3659  sbc2or  3739  csbiegf  3871  un00  4380  elimhyp  4527  elimhyp2v  4528  elimhyp3v  4529  elimhyp4v  4530  elimdhyp  4532  keephyp2v  4534  keephyp3v  4535  preq12b  4788  nfopd  4828  ssex  5256  opthwiener  5462  isso2i  5570  nfimad  6028  dfrel2  6147  ordtri3or  6349  on0eqel  6442  funsng  6543  cnvresid  6571  nffvd  6846  fnbrfvb  6884  fvelrnb  6894  fvelimab  6906  funfvop  6998  fvsnun2  7134  iunpw  7721  onsucuni  7775  onuninsuci  7787  tposf12  8198  oaword1  8484  oneo  8513  nnaword1  8562  nnneo  8588  naddword1  8624  1sdom2dom  9161  inficl  9335  fipwuni  9336  infeq5i  9555  cantnflt  9591  cantnflem1  9608  cnfcom  9619  brttrcl  9632  rankidn  9744  rankr1id  9784  rankxpsuc  9804  iscard  9897  iscard2  9898  carduni  9903  cardmin2  9921  infxpenlem  9933  alephgeom  10002  cardaleph  10009  infenaleph  10011  iscard3  10013  alephsson  10020  alephfp  10028  alephval3  10030  dfac12k  10068  axdc3lem2  10371  alephval2  10493  alephreg  10503  cfpwsdom  10505  alephom  10506  axrepndlem1  10513  axunndlem1  10516  axunnd  10517  axpowndlem2  10519  axpowndlem3  10520  axpowndlem4  10521  axpownd  10522  axregndlem2  10524  axinfndlem1  10526  axinfnd  10527  axacndlem4  10531  axacndlem5  10532  axacnd  10533  gchaleph2  10593  elwina  10607  elina  10608  winaon  10609  inawina  10611  winainf  10615  winalim  10616  tskr1om2  10689  r1tskina  10703  gruina  10739  grur1a  10740  indpi  10828  nqerrel  10853  recidnq  10886  ltaddnq  10895  pncan3  11399  divcan2  11815  ltp1  11993  ltm1  11995  recreclt  12053  elnn0z  12535  nn0ind-raph  12627  fzdifsuc  13536  2tnp1ge0ge0  13786  fsuppmapnn0fiubex  13952  faclbnd5  14258  hashfun  14397  ccatalpha  14554  caucvgrlem  15633  fsumcnv  15733  fprodcnv  15946  ef01bndlem  16149  sin01gt0  16155  cos01gt0  16156  egt2lt3  16171  cnso  16212  ltoddhalfle  16328  4sqlem12  16925  funcres  17861  fuchom  17929  xpsmnd  18743  xpsgrp  19033  mulgfval  19043  mulgfvalALT  19044  nmznsg  19141  frgp0  19733  gsumval3lem2  19879  gsumval3  19880  xpsrngd  20158  xpsringd  20310  pwssplit1  21056  pzriprnglem4  21466  mvrf1  21967  psdmul  22161  ply1chr  22299  blssioo  24785  dvidlem  25907  dvcj  25942  dvrec  25947  rolle  25982  cmvth  25983  mvth  25984  dvlip  25985  dvlipcn  25986  dv11cn  25993  dvivthlem2  26001  lhop1lem  26005  lhop1  26006  lhop2  26007  q1peqb  26146  pserdv  26419  sinhalfpilem  26452  tangtx  26494  efabl  26539  logi  26576  logneg2  26604  gausslemma2dlem1a  27353  lgseisenlem4  27366  2lgslem3a  27384  2lgslem3b  27385  2lgslem3c  27386  2lgslem3d  27387  dchrisum0lem3  27507  mulogsum  27520  pntrlog2bndlem1  27565  madebday  27917  ltsp1d  28032  pncan3s  28090  divscan2wd  28214  om2noseqoi  28320  n0sge0  28355  bdayfinbndlem1  28484  1reno  28514  axlowdimlem7  29042  axlowdimlem10  29045  axcontlem6  29063  umgrbi  29195  rusgr1vtxlem  29681  clwwlknonwwlknonb  30201  3wlkond  30266  frcond3  30364  hsn0elch  31344  axpjcl  31496  omlsilem  31498  pjchi  31528  shs00i  31546  chj00i  31583  chabs1  31612  pjspansn  31673  chscllem1  31733  osumcor2i  31740  nonbooli  31747  atcvat4i  32493  xppreima  32744  xdivrec  33012  wrdt2ind  33039  psgndmfi  33186  sqsscirc1  34099  1stmbfm  34451  2ndmbfm  34452  carsgclctunlem2  34510  eulerpartlemgh  34569  hgt750leme  34849  bnj1148  35185  bnj1154  35188  fineqvpow  35303  fineqvacALT  35305  fineqvnttrclse  35312  fineqvr1ombregs  35326  cvmlift3lem5  35558  cvmlift3lem7  35560  currybi  35923  dfon2lem3  36018  dfon2lem7  36022  distel  36036  altopthsn  36196  axtcond  36713  ttc00  36743  bj-ax12  37004  bj-exlimmpbi  37273  irrdiff  37693  rdgssun  37747  wl-ax12v2cl  37875  poimirlem9  38003  poimirlem26  38020  poimirlem27  38021  poimirlem32  38026  dvasin  38078  areacirclem4  38085  heiborlem8  38192  0rngo  38401  dfsuccl4  38848  suceldisj  39192  ax12eq  39440  ax12el  39441  ax12inda  39447  ax12v2-o  39448  nfded  39466  nfded2  39467  nfunidALT2  39468  lshpinN  39488  trlid0  40675  hdmap10lem  42338  lcmineqlem  42544  aks4d1p1p5  42567  fisdomnn  42735  asin1half  42841  renegid  42857  repncan3  42867  sn-00idlem2  42883  reixi  42907  rerecne0d  42940  sn-ltp1  42973  flt4lem7  43116  islssfg2  43523  areaquad  43668  onsupuni  43681  onov0suclim  43726  minregex  43985  wfac8prim  45453  fperdvper  46369  itgvol0  46418  stoweidlem13  46463  stoweidlem26  46476  stoweidlem34  46484  wallispilem4  46518  dirkercncflem1  46553  dirkercncflem3  46555  dirkercncflem4  46556  fourierdlem35  46592  fourierdlem73  46629  funressndmafv2rn  47693  dfatbrafv2b  47715  fnbrafv2b  47718  ichnfimlem  47945  lighneallem4b  48094  nprmdvdsfacm1lem4  48108  sbgoldbwt  48275  sbgoldbalt  48279  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  bgoldbtbndlem1  48303  bgoldbtbndlem3  48305  grimidvtxedg  48383  tposideq  49385  iooii  49415  0thincg  49955  oduoppcciso  50063