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  2769  eqvisset  3474  vtoclg  3521  vtocl  3524  vtoclf  3529  vtoclgf  3533  vtoclg1f  3534  eueq3  3672  sbc2or  3751  csbiegf  3884  un00  4360  vvin  4362  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elimdhyp  4556  keephyp2v  4558  keephyp3v  4559  preq12b  4808  nfopd  4853  ssexOLD  5287  opthwiener  5491  isso2i  5600  nfimad  6077  dfrel2  6193  ordtri3or  6413  on0eqel  6506  funsng  6613  cnvresidOLD  6641  nffvd  6920  fnbrfvb  6958  fvelrnb  6968  fvelimab  6980  funfvop  7072  fvsnun2  7211  iunpw  7809  onsucuni  7863  onuninsuci  7875  tposf12  8296  oaword1  8588  oneo  8617  nnaword1  8666  nnneo  8692  naddword1  8729  1sdom2dom  9273  inficl  9444  fipwuni  9445  infeq5i  9664  cantnflt  9700  cantnflem1  9717  cnfcom  9728  brttrcl  9741  rankidn  9858  rankr1id  9905  rankxpsuc  9926  iscard  10083  iscard2  10084  carduni  10089  cardmin2  10107  infxpenlem  10119  alephgeom  10188  cardaleph  10195  infenaleph  10197  iscard3  10199  alephsson  10206  alephfp  10214  alephval3  10216  dfac12k  10253  axdc3lem2  10556  alephval2  10684  alephreg  10694  cfpwsdom  10696  alephom  10697  axrepndlem1  10704  axunndlem1  10707  axunnd  10708  axpowndlem2  10710  axpowndlem3  10711  axpowndlem4  10712  axpownd  10713  axregndlem2  10715  axinfndlem1  10717  axinfnd  10718  axacndlem4  10722  axacndlem5  10723  axacnd  10724  gchaleph2  10784  elwina  10798  elina  10799  winaon  10800  inawina  10802  winainf  10806  winalim  10807  tskhf  10880  r1tskina  10894  gruina  10930  grur1a  10931  indpi  11019  nqerrel  11044  recidnq  11077  ltaddnq  11086  pncan3  11592  divcan2  12009  ltp1  12184  ltm1  12186  recreclt  12243  elnn0z  12733  nn0ind-raph  12826  fzdifsuc  13745  2tnp1ge0ge0  13996  fsuppmapnn0fiubex  14162  faclbnd5  14469  hashfun  14609  ccatalpha  14767  caucvgrlem  15869  fsumcnv  15968  fprodcnv  16179  ef01bndlem  16381  sin01gt0  16387  cos01gt0  16388  egt2lt3  16403  cnso  16444  ltoddhalfle  16560  4sqlem12  17163  funcres  18100  fuchom  18168  xpsmnd  19000  xpsgrp  19298  mulgfval  19308  mulgfvalALT  19309  nmznsg  19407  frgp0  20004  gsumval3lem2  20150  gsumval3  20151  xpsrngd  20431  xpsringd  20592  pwssplit1  21364  pzriprnglem4  21820  mvrf1  22323  psdmul  22517  ply1chr  22654  blssioo  25144  dvidlem  26265  dvcj  26300  dvrec  26305  rolle  26340  cmvth  26341  mvth  26342  dvlip  26343  dvlipcn  26344  dv11cn  26351  dvivthlem2  26359  lhop1lem  26363  lhop1  26364  lhop2  26365  q1peqb  26504  pserdv  26786  sinhalfpilem  26822  tangtx  26864  efabl  26908  logi  26945  logneg2  26973  gausslemma2dlem1a  27722  lgseisenlem4  27735  2lgslem3a  27753  2lgslem3b  27754  2lgslem3c  27755  2lgslem3d  27756  dchrisum0lem3  27876  mulogsum  27889  pntrlog2bndlem1  27934  flt4lem7  28019  madebday  28316  ltsp1d  28431  pncan3s  28489  divscan2wd  28613  om2noseqoi  28719  n0sge0  28754  bdayfinbndlem1  28883  1reno  28913  prlngsymquadlem  29471  axlowdimlem7  29556  axlowdimlem10  29559  axcontlem6  29577  umgrbi  29709  rusgr1vtxlem  30198  clwwlknonwwlknonb  30727  3wlkond  30802  frcond3  30900  hsn0elch  31880  axpjcl  32032  omlsilem  32034  pjchi  32064  shs00i  32082  chj00i  32119  chabs1  32148  pjspansn  32209  chscllem1  32269  osumcor2i  32276  nonbooli  32283  atcvat4i  33029  xppreima  33311  xdivrec  33563  wrdt2ind  33586  psgndmfi  33729  sqsscirc1  34610  1stmbfm  34962  2ndmbfm  34963  carsgclctunlem2  35021  eulerpartlemgh  35080  hgt750leme  35357  bnj1148  35696  bnj1154  35699  fineqvpow  35883  fineqvacALT  35885  fineqvnttrclse  35892  fineqvhfbregs  35906  gdlopcfvlem  35971  cvmlift3lem5  36255  cvmlift3lem7  36257  currybi  36620  dfon2lem3  36725  dfon2lem7  36729  distel  36743  altopthsn  36904  axtcond  37444  ttc00  37474  bj-ax12  37734  bj-exlimmpbi  38003  irrdiff  38439  rdgssun  38493  wl-ax12v2cl  38621  poimirlem9  38739  poimirlem26  38756  poimirlem27  38757  poimirlem32  38762  dvasin  38814  areacirclem4  38821  heiborlem8  38944  0rngo  39153  dfsuccl4  39598  suceldisj  39942  ax12eq  40190  ax12el  40191  ax12inda  40197  ax12v2-o  40198  nfded  40216  nfded2  40217  nfunidALT2  40218  lshpinN  40238  trlid0  41425  hdmap10lem  43088  lcmineqlem  43294  aks4d1p1p5  43317  fisdomnn  43488  asin1half  43601  renegid  43617  repncan3  43627  sn-00idlem2  43643  reixi  43667  rerecne0d  43700  sn-ltp1  43733  islssfg2  44266  areaquad  44410  onsupuni  44423  onov0suclim  44468  minregex  44727  wfac8prim  46187  fperdvper  47134  itgvol0  47183  stoweidlem13  47228  stoweidlem26  47241  stoweidlem34  47249  wallispilem4  47283  dirkercncflem1  47318  dirkercncflem3  47320  dirkercncflem4  47321  fourierdlem35  47357  fourierdlem73  47394  goldratval  48141  funressndmafv2rn  48498  dfatbrafv2b  48520  fnbrafv2b  48523  ichnfimlem  48750  lighneallem4b  48899  nprmdvdsfacm1lem4  48913  sbgoldbwt  49080  sbgoldbalt  49084  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  bgoldbtbndlem1  49108  bgoldbtbndlem3  49110  grimidvtxedg  49188  tposideq  50206  iooii  50237  0thincg  50798  oduoppcciso  50909