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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  dedt  1100  eqcomd  2766  eqvisset  3470  vtoclg  3517  vtocl  3520  vtoclf  3525  vtoclgf  3529  vtoclg1f  3530  eueq3  3668  sbc2or  3747  csbiegf  3879  un00  4356  vvin  4358  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  preq12b  4804  nfopd  4849  ssexOLD  5282  opthwiener  5486  isso2i  5595  nfimad  6064  dfrel2  6180  ordtri3or  6395  on0eqel  6488  funsng  6591  cnvresid  6619  nffvd  6897  fnbrfvb  6935  fvelrnb  6945  fvelimab  6957  funfvop  7049  fvsnun2  7188  iunpw  7785  onsucuni  7839  onuninsuci  7851  tposf12  8271  oaword1  8563  oneo  8592  nnaword1  8641  nnneo  8667  naddword1  8704  1sdom2dom  9248  inficl  9420  fipwuni  9421  infeq5i  9640  cantnflt  9676  cantnflem1  9693  cnfcom  9704  brttrcl  9717  rankidn  9834  rankr1id  9881  rankxpsuc  9902  iscard  10059  iscard2  10060  carduni  10065  cardmin2  10083  infxpenlem  10095  alephgeom  10164  cardaleph  10171  infenaleph  10173  iscard3  10175  alephsson  10182  alephfp  10190  alephval3  10192  dfac12k  10229  axdc3lem2  10532  alephval2  10660  alephreg  10670  cfpwsdom  10672  alephom  10673  axrepndlem1  10680  axunndlem1  10683  axunnd  10684  axpowndlem2  10686  axpowndlem3  10687  axpowndlem4  10688  axpownd  10689  axregndlem2  10691  axinfndlem1  10693  axinfnd  10694  axacndlem4  10698  axacndlem5  10699  axacnd  10700  gchaleph2  10760  elwina  10774  elina  10775  winaon  10776  inawina  10778  winainf  10782  winalim  10783  tskhf  10856  r1tskina  10870  gruina  10906  grur1a  10907  indpi  10995  nqerrel  11020  recidnq  11053  ltaddnq  11062  pncan3  11568  divcan2  11985  ltp1  12160  ltm1  12162  recreclt  12219  elnn0z  12709  nn0ind-raph  12802  fzdifsuc  13721  2tnp1ge0ge0  13972  fsuppmapnn0fiubex  14138  faclbnd5  14445  hashfun  14585  ccatalpha  14743  caucvgrlem  15845  fsumcnv  15944  fprodcnv  16155  ef01bndlem  16357  sin01gt0  16363  cos01gt0  16364  egt2lt3  16379  cnso  16420  ltoddhalfle  16536  4sqlem12  17139  funcres  18076  fuchom  18144  xpsmnd  18976  xpsgrp  19274  mulgfval  19284  mulgfvalALT  19285  nmznsg  19383  frgp0  19979  gsumval3lem2  20125  gsumval3  20126  xpsrngd  20406  xpsringd  20567  pwssplit1  21339  pzriprnglem4  21795  mvrf1  22298  psdmul  22492  ply1chr  22629  blssioo  25119  dvidlem  26240  dvcj  26275  dvrec  26280  rolle  26315  cmvth  26316  mvth  26317  dvlip  26318  dvlipcn  26319  dv11cn  26326  dvivthlem2  26334  lhop1lem  26338  lhop1  26339  lhop2  26340  q1peqb  26479  pserdv  26761  sinhalfpilem  26797  tangtx  26839  efabl  26883  logi  26920  logneg2  26948  gausslemma2dlem1a  27697  lgseisenlem4  27710  2lgslem3a  27728  2lgslem3b  27729  2lgslem3c  27730  2lgslem3d  27731  dchrisum0lem3  27851  mulogsum  27864  pntrlog2bndlem1  27909  flt4lem7  27994  madebday  28291  ltsp1d  28406  pncan3s  28464  divscan2wd  28588  om2noseqoi  28694  n0sge0  28729  bdayfinbndlem1  28858  1reno  28888  prlngsymquadlem  29446  axlowdimlem7  29531  axlowdimlem10  29534  axcontlem6  29552  umgrbi  29684  rusgr1vtxlem  30173  clwwlknonwwlknonb  30702  3wlkond  30777  frcond3  30875  hsn0elch  31855  axpjcl  32007  omlsilem  32009  pjchi  32039  shs00i  32057  chj00i  32094  chabs1  32123  pjspansn  32184  chscllem1  32244  osumcor2i  32251  nonbooli  32258  atcvat4i  33004  xppreima  33286  xdivrec  33539  wrdt2ind  33562  psgndmfi  33705  sqsscirc1  34586  1stmbfm  34938  2ndmbfm  34939  carsgclctunlem2  34997  eulerpartlemgh  35056  hgt750leme  35333  bnj1148  35672  bnj1154  35675  fineqvpow  35839  fineqvacALT  35841  fineqvnttrclse  35848  fineqvr1ombregs  35862  cvmlift3lem5  36174  cvmlift3lem7  36176  currybi  36539  dfon2lem3  36639  dfon2lem7  36643  distel  36657  altopthsn  36818  axtcond  37358  ttc00  37388  bj-ax12  37648  bj-exlimmpbi  37917  irrdiff  38340  rdgssun  38394  wl-ax12v2cl  38522  poimirlem9  38640  poimirlem26  38657  poimirlem27  38658  poimirlem32  38663  dvasin  38715  areacirclem4  38722  heiborlem8  38845  0rngo  39054  dfsuccl4  39499  suceldisj  39843  ax12eq  40091  ax12el  40092  ax12inda  40098  ax12v2-o  40099  nfded  40117  nfded2  40118  nfunidALT2  40119  lshpinN  40139  trlid0  41326  hdmap10lem  42989  lcmineqlem  43195  aks4d1p1p5  43218  fisdomnn  43388  asin1half  43501  renegid  43517  repncan3  43527  sn-00idlem2  43543  reixi  43567  rerecne0d  43600  sn-ltp1  43633  islssfg2  44166  areaquad  44311  onsupuni  44324  onov0suclim  44369  minregex  44628  wfac8prim  46085  fperdvper  47022  itgvol0  47071  stoweidlem13  47116  stoweidlem26  47129  stoweidlem34  47137  wallispilem4  47171  dirkercncflem1  47206  dirkercncflem3  47208  dirkercncflem4  47209  fourierdlem35  47245  fourierdlem73  47282  goldratval  48029  funressndmafv2rn  48386  dfatbrafv2b  48408  fnbrafv2b  48411  ichnfimlem  48638  lighneallem4b  48787  nprmdvdsfacm1lem4  48801  sbgoldbwt  48968  sbgoldbalt  48972  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  bgoldbtbndlem1  48996  bgoldbtbndlem3  48998  grimidvtxedg  49076  tposideq  50094  iooii  50125  0thincg  50686  oduoppcciso  50797