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  4811  nfopd  4851  ssex  5282  opthwiener  5488  isso2i  5597  nfimad  6062  dfrel2  6179  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  12046  ltm1  12048  recreclt  12105  elnn0z  12595  nn0ind-raph  12687  fzdifsuc  13603  2tnp1ge0ge0  13853  fsuppmapnn0fiubex  14019  faclbnd5  14325  hashfun  14464  ccatalpha  14621  caucvgrlem  15714  fsumcnv  15814  fprodcnv  16027  ef01bndlem  16230  sin01gt0  16236  cos01gt0  16237  egt2lt3  16252  cnso  16293  ltoddhalfle  16409  4sqlem12  17006  funcres  17943  fuchom  18011  xpsmnd  18825  xpsgrp  19116  mulgfval  19126  mulgfvalALT  19127  nmznsg  19225  frgp0  19821  gsumval3lem2  19967  gsumval3  19968  xpsrngd  20248  xpsringd  20405  pwssplit1  21149  pzriprnglem4  21594  mvrf1  22095  psdmul  22289  ply1chr  22427  blssioo  24913  dvidlem  26035  dvcj  26070  dvrec  26075  rolle  26110  cmvth  26111  mvth  26112  dvlip  26113  dvlipcn  26114  dv11cn  26121  dvivthlem2  26129  lhop1lem  26133  lhop1  26134  lhop2  26135  q1peqb  26274  pserdv  26550  sinhalfpilem  26586  tangtx  26628  efabl  26673  logi  26710  logneg2  26738  gausslemma2dlem1a  27487  lgseisenlem4  27500  2lgslem3a  27518  2lgslem3b  27519  2lgslem3c  27520  2lgslem3d  27521  dchrisum0lem3  27641  mulogsum  27654  pntrlog2bndlem1  27699  madebday  28051  ltsp1d  28166  pncan3s  28224  divscan2wd  28348  om2noseqoi  28454  n0sge0  28489  bdayfinbndlem1  28618  1reno  28648  axlowdimlem7  29207  axlowdimlem10  29210  axcontlem6  29228  umgrbi  29360  rusgr1vtxlem  29846  clwwlknonwwlknonb  30366  3wlkond  30431  frcond3  30529  hsn0elch  31509  axpjcl  31661  omlsilem  31663  pjchi  31693  shs00i  31711  chj00i  31748  chabs1  31777  pjspansn  31838  chscllem1  31898  osumcor2i  31905  nonbooli  31912  atcvat4i  32658  xppreima  32902  xdivrec  33159  wrdt2ind  33186  psgndmfi  33331  sqsscirc1  34215  1stmbfm  34567  2ndmbfm  34568  carsgclctunlem2  34626  eulerpartlemgh  34685  hgt750leme  34962  bnj1148  35301  bnj1154  35304  fineqvpow  35423  fineqvacALT  35425  fineqvnttrclse  35432  fineqvr1ombregs  35446  cvmlift3lem5  35686  cvmlift3lem7  35688  currybi  36051  dfon2lem3  36146  dfon2lem7  36150  distel  36164  altopthsn  36324  axtcond  36851  ttc00  36881  bj-ax12  37141  bj-exlimmpbi  37410  irrdiff  37830  rdgssun  37884  wl-ax12v2cl  38012  poimirlem9  38140  poimirlem26  38157  poimirlem27  38158  poimirlem32  38163  dvasin  38215  areacirclem4  38222  heiborlem8  38329  0rngo  38538  dfsuccl4  38985  suceldisj  39329  ax12eq  39577  ax12el  39578  ax12inda  39584  ax12v2-o  39585  nfded  39603  nfded2  39604  nfunidALT2  39605  lshpinN  39625  trlid0  40812  hdmap10lem  42475  lcmineqlem  42681  aks4d1p1p5  42704  fisdomnn  42872  asin1half  42978  renegid  42994  repncan3  43004  sn-00idlem2  43020  reixi  43044  rerecne0d  43077  sn-ltp1  43110  flt4lem7  43253  islssfg2  43660  areaquad  43805  onsupuni  43818  onov0suclim  43863  minregex  44122  wfac8prim  45576  fperdvper  46491  itgvol0  46540  stoweidlem13  46585  stoweidlem26  46598  stoweidlem34  46606  wallispilem4  46640  dirkercncflem1  46675  dirkercncflem3  46677  dirkercncflem4  46678  fourierdlem35  46714  fourierdlem73  46751  funressndmafv2rn  47815  dfatbrafv2b  47837  fnbrafv2b  47840  ichnfimlem  48067  lighneallem4b  48216  nprmdvdsfacm1lem4  48230  sbgoldbwt  48397  sbgoldbalt  48401  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  bgoldbtbndlem1  48425  bgoldbtbndlem3  48427  grimidvtxedg  48505  tposideq  49517  iooii  49547  0thincg  50087  oduoppcciso  50195