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  1100  eqcomd  2769  eqvisset  3475  vtoclg  3523  vtocl  3526  vtoclf  3531  vtoclgf  3535  vtoclg1f  3536  eueq3  3675  sbc2or  3754  csbiegf  3887  un00  4365  vvin  4367  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elimdhyp  4559  keephyp2v  4561  keephyp3v  4562  preq12b  4816  nfopd  4856  ssexOLD  5293  opthwiener  5499  isso2i  5608  nfimad  6073  dfrel2  6189  ordtri3or  6395  on0eqel  6488  funsng  6589  cnvresid  6617  nffvd  6895  fnbrfvb  6933  fvelrnb  6943  fvelimab  6955  funfvop  7047  fvsnun2  7183  iunpw  7771  onsucuni  7825  onuninsuci  7837  tposf12  8248  oaword1  8538  oneo  8567  nnaword1  8616  nnneo  8642  naddword1  8679  1sdom2dom  9215  inficl  9386  fipwuni  9387  infeq5i  9606  cantnflt  9642  cantnflem1  9659  cnfcom  9670  brttrcl  9683  rankidn  9795  rankr1id  9835  rankxpsuc  9855  iscard  9962  iscard2  9963  carduni  9968  cardmin2  9986  infxpenlem  9998  alephgeom  10067  cardaleph  10074  infenaleph  10076  iscard3  10078  alephsson  10085  alephfp  10093  alephval3  10095  dfac12k  10132  axdc3lem2  10436  alephval2  10558  alephreg  10568  cfpwsdom  10570  alephom  10571  axrepndlem1  10578  axunndlem1  10581  axunnd  10582  axpowndlem2  10584  axpowndlem3  10585  axpowndlem4  10586  axpownd  10587  axregndlem2  10589  axinfndlem1  10591  axinfnd  10592  axacndlem4  10596  axacndlem5  10597  axacnd  10598  gchaleph2  10658  elwina  10672  elina  10673  winaon  10674  inawina  10676  winainf  10680  winalim  10681  tskr1om2  10754  r1tskina  10768  gruina  10804  grur1a  10805  indpi  10893  nqerrel  10918  recidnq  10951  ltaddnq  10960  pncan3  11466  divcan2  11881  ltp1  12056  ltm1  12058  recreclt  12115  elnn0z  12605  nn0ind-raph  12697  fzdifsuc  13614  2tnp1ge0ge0  13864  fsuppmapnn0fiubex  14030  faclbnd5  14336  hashfun  14476  ccatalpha  14633  caucvgrlem  15726  fsumcnv  15826  fprodcnv  16039  ef01bndlem  16241  sin01gt0  16247  cos01gt0  16248  egt2lt3  16263  cnso  16304  ltoddhalfle  16420  4sqlem12  17017  funcres  17954  fuchom  18022  xpsmnd  18836  xpsgrp  19126  mulgfval  19136  mulgfvalALT  19137  nmznsg  19235  frgp0  19831  gsumval3lem2  19977  gsumval3  19978  xpsrngd  20258  xpsringd  20415  pwssplit1  21161  pzriprnglem4  21615  mvrf1  22116  psdmul  22310  ply1chr  22447  blssioo  24933  dvidlem  26055  dvcj  26090  dvrec  26095  rolle  26130  cmvth  26131  mvth  26132  dvlip  26133  dvlipcn  26134  dv11cn  26141  dvivthlem2  26149  lhop1lem  26153  lhop1  26154  lhop2  26155  q1peqb  26294  pserdv  26570  sinhalfpilem  26606  tangtx  26648  efabl  26693  logi  26730  logneg2  26758  gausslemma2dlem1a  27507  lgseisenlem4  27520  2lgslem3a  27538  2lgslem3b  27539  2lgslem3c  27540  2lgslem3d  27541  dchrisum0lem3  27661  mulogsum  27674  pntrlog2bndlem1  27719  madebday  28071  ltsp1d  28186  pncan3s  28244  divscan2wd  28368  om2noseqoi  28474  n0sge0  28509  bdayfinbndlem1  28638  1reno  28668  prlngsymquadlem  29191  axlowdimlem7  29276  axlowdimlem10  29279  axcontlem6  29297  umgrbi  29429  rusgr1vtxlem  29915  clwwlknonwwlknonb  30435  3wlkond  30500  frcond3  30598  hsn0elch  31578  axpjcl  31730  omlsilem  31732  pjchi  31762  shs00i  31780  chj00i  31817  chabs1  31846  pjspansn  31907  chscllem1  31967  osumcor2i  31974  nonbooli  31981  atcvat4i  32727  xppreima  32968  xdivrec  33224  wrdt2ind  33251  psgndmfi  33396  sqsscirc1  34276  1stmbfm  34628  2ndmbfm  34629  carsgclctunlem2  34687  eulerpartlemgh  34746  hgt750leme  35023  bnj1148  35362  bnj1154  35365  fineqvpow  35506  fineqvacALT  35508  fineqvnttrclse  35515  fineqvr1ombregs  35529  cvmlift3lem5  35793  cvmlift3lem7  35795  currybi  36158  dfon2lem3  36253  dfon2lem7  36257  distel  36271  altopthsn  36431  axtcond  36967  ttc00  36997  bj-ax12  37257  bj-exlimmpbi  37526  irrdiff  37948  rdgssun  38002  wl-ax12v2cl  38130  poimirlem9  38258  poimirlem26  38275  poimirlem27  38276  poimirlem32  38281  dvasin  38333  areacirclem4  38340  heiborlem8  38447  0rngo  38656  dfsuccl4  39101  suceldisj  39445  ax12eq  39693  ax12el  39694  ax12inda  39700  ax12v2-o  39701  nfded  39719  nfded2  39720  nfunidALT2  39721  lshpinN  39741  trlid0  40928  hdmap10lem  42591  lcmineqlem  42797  aks4d1p1p5  42820  fisdomnn  42990  asin1half  43096  renegid  43112  repncan3  43122  sn-00idlem2  43138  reixi  43162  rerecne0d  43195  sn-ltp1  43228  flt4lem7  43371  islssfg2  43778  areaquad  43923  onsupuni  43936  onov0suclim  43981  minregex  44240  wfac8prim  45691  fperdvper  46613  itgvol0  46662  stoweidlem13  46707  stoweidlem26  46720  stoweidlem34  46728  wallispilem4  46762  dirkercncflem1  46797  dirkercncflem3  46799  dirkercncflem4  46800  fourierdlem35  46836  fourierdlem73  46873  funressndmafv2rn  47937  dfatbrafv2b  47959  fnbrafv2b  47962  ichnfimlem  48189  lighneallem4b  48338  nprmdvdsfacm1lem4  48352  sbgoldbwt  48519  sbgoldbalt  48523  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  bgoldbtbndlem1  48547  bgoldbtbndlem3  48549  grimidvtxedg  48627  tposideq  49643  iooii  49673  0thincg  50213  oduoppcciso  50321