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  1098  eqcomd  2771  eqvisset  3477  vtoclg  3525  vtocl  3528  vtoclf  3533  vtoclgf  3537  vtoclg1f  3538  eueq3  3677  sbc2or  3756  csbiegf  3888  un00  4402  elimhyp  4549  elimhyp2v  4550  elimhyp3v  4551  elimhyp4v  4552  elimdhyp  4554  keephyp2v  4556  keephyp3v  4557  preq12b  4810  nfopd  4850  ssex  5281  opthwiener  5487  isso2i  5596  nfimad  6061  dfrel2  6178  ordtri3or  6382  on0eqel  6475  funsng  6576  cnvresid  6604  nffvd  6883  fnbrfvb  6921  fvelrnb  6931  fvelimab  6943  funfvop  7035  fvsnun2  7171  iunpw  7758  onsucuni  7812  onuninsuci  7824  tposf12  8235  oaword1  8525  oneo  8554  nnaword1  8603  nnneo  8629  naddword1  8666  1sdom2dom  9202  inficl  9373  fipwuni  9374  infeq5i  9593  cantnflt  9629  cantnflem1  9646  cnfcom  9657  brttrcl  9670  rankidn  9782  rankr1id  9822  rankxpsuc  9842  iscard  9949  iscard2  9950  carduni  9955  cardmin2  9973  infxpenlem  9985  alephgeom  10054  cardaleph  10061  infenaleph  10063  iscard3  10065  alephsson  10072  alephfp  10080  alephval3  10082  dfac12k  10119  axdc3lem2  10423  alephval2  10545  alephreg  10555  cfpwsdom  10557  alephom  10558  axrepndlem1  10565  axunndlem1  10568  axunnd  10569  axpowndlem2  10571  axpowndlem3  10572  axpowndlem4  10573  axpownd  10574  axregndlem2  10576  axinfndlem1  10578  axinfnd  10579  axacndlem4  10583  axacndlem5  10584  axacnd  10585  gchaleph2  10645  elwina  10659  elina  10660  winaon  10661  inawina  10663  winainf  10667  winalim  10668  tskr1om2  10741  r1tskina  10755  gruina  10791  grur1a  10792  indpi  10880  nqerrel  10905  recidnq  10938  ltaddnq  10947  pncan3  11453  divcan2  11868  ltp1  12043  ltm1  12045  recreclt  12102  elnn0z  12592  nn0ind-raph  12684  fzdifsuc  13600  2tnp1ge0ge0  13850  fsuppmapnn0fiubex  14016  faclbnd5  14322  hashfun  14462  ccatalpha  14619  caucvgrlem  15712  fsumcnv  15812  fprodcnv  16025  ef01bndlem  16228  sin01gt0  16234  cos01gt0  16235  egt2lt3  16250  cnso  16291  ltoddhalfle  16407  4sqlem12  17004  funcres  17941  fuchom  18009  xpsmnd  18823  xpsgrp  19113  mulgfval  19123  mulgfvalALT  19124  nmznsg  19222  frgp0  19818  gsumval3lem2  19964  gsumval3  19965  xpsrngd  20245  xpsringd  20402  pwssplit1  21146  pzriprnglem4  21591  mvrf1  22092  psdmul  22286  ply1chr  22423  blssioo  24909  dvidlem  26031  dvcj  26066  dvrec  26071  rolle  26106  cmvth  26107  mvth  26108  dvlip  26109  dvlipcn  26110  dv11cn  26117  dvivthlem2  26125  lhop1lem  26129  lhop1  26130  lhop2  26131  q1peqb  26270  pserdv  26546  sinhalfpilem  26582  tangtx  26624  efabl  26669  logi  26706  logneg2  26734  gausslemma2dlem1a  27483  lgseisenlem4  27496  2lgslem3a  27514  2lgslem3b  27515  2lgslem3c  27516  2lgslem3d  27517  dchrisum0lem3  27637  mulogsum  27650  pntrlog2bndlem1  27695  madebday  28047  ltsp1d  28162  pncan3s  28220  divscan2wd  28344  om2noseqoi  28450  n0sge0  28485  bdayfinbndlem1  28614  1reno  28644  axlowdimlem7  29203  axlowdimlem10  29206  axcontlem6  29224  umgrbi  29356  rusgr1vtxlem  29842  clwwlknonwwlknonb  30362  3wlkond  30427  frcond3  30525  hsn0elch  31505  axpjcl  31657  omlsilem  31659  pjchi  31689  shs00i  31707  chj00i  31744  chabs1  31773  pjspansn  31834  chscllem1  31894  osumcor2i  31901  nonbooli  31908  atcvat4i  32654  xppreima  32898  xdivrec  33154  wrdt2ind  33181  psgndmfi  33326  sqsscirc1  34210  1stmbfm  34562  2ndmbfm  34563  carsgclctunlem2  34621  eulerpartlemgh  34680  hgt750leme  34957  bnj1148  35296  bnj1154  35299  fineqvpow  35418  fineqvacALT  35420  fineqvnttrclse  35427  fineqvr1ombregs  35441  cvmlift3lem5  35681  cvmlift3lem7  35683  currybi  36046  dfon2lem3  36141  dfon2lem7  36145  distel  36159  altopthsn  36319  axtcond  36846  ttc00  36876  bj-ax12  37136  bj-exlimmpbi  37405  irrdiff  37825  rdgssun  37879  wl-ax12v2cl  38007  poimirlem9  38135  poimirlem26  38152  poimirlem27  38153  poimirlem32  38158  dvasin  38210  areacirclem4  38217  heiborlem8  38324  0rngo  38533  dfsuccl4  38980  suceldisj  39324  ax12eq  39572  ax12el  39573  ax12inda  39579  ax12v2-o  39580  nfded  39598  nfded2  39599  nfunidALT2  39600  lshpinN  39620  trlid0  40807  hdmap10lem  42470  lcmineqlem  42676  aks4d1p1p5  42699  fisdomnn  42867  asin1half  42973  renegid  42989  repncan3  42999  sn-00idlem2  43015  reixi  43039  rerecne0d  43072  sn-ltp1  43105  flt4lem7  43248  islssfg2  43655  areaquad  43800  onsupuni  43813  onov0suclim  43858  minregex  44117  wfac8prim  45570  fperdvper  46492  itgvol0  46541  stoweidlem13  46586  stoweidlem26  46599  stoweidlem34  46607  wallispilem4  46641  dirkercncflem1  46676  dirkercncflem3  46678  dirkercncflem4  46679  fourierdlem35  46715  fourierdlem73  46752  funressndmafv2rn  47816  dfatbrafv2b  47838  fnbrafv2b  47841  ichnfimlem  48068  lighneallem4b  48217  nprmdvdsfacm1lem4  48231  sbgoldbwt  48398  sbgoldbalt  48402  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  bgoldbtbndlem1  48426  bgoldbtbndlem3  48428  grimidvtxedg  48506  tposideq  49518  iooii  49548  0thincg  50088  oduoppcciso  50196