Theorem mpbii 222

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  elimh  1024  elimhOLD  1027  axc15  2291  ax12v2OLD  2330  eqcomd  2616  eqvisset  3184  vtoclgf  3237  vtoclg1f  3238  eueq3  3348  sbc2or  3411  csbiegf  3523  un00  3963  elimhyp  4096  elimhyp2v  4097  elimhyp3v  4098  elimhyp4v  4099  elimdhyp  4101  keephyp2v  4103  keephyp3v  4104  preqr1OLD  4320  preq12b  4322  prel12  4323  nfopd  4357  ssex  4730  opthwiener  4901  isso2i  4991  nfimad  5394  dfrel2  5502  ordtri3or  5672  on0eqel  5762  funsng  5851  cnvresid  5882  nffvd  6112  fnbrfvb  6146  fvelrnb  6153  fvelimab  6163  funfvop  6237  iunpw  6870  onsucuni  6920  onuninsuci  6932  tposf12  7264  oaword1  7519  oneo  7548  nnaword1  7596  nnneo  7618  inficl  8214  fipwuni  8215  infeq5i  8416  cantnflt  8452  cantnflem1  8469  cnfcom  8480  rankidn  8568  rankr1id  8608  rankxpsuc  8628  iscard  8684  iscard2  8685  carduni  8690  cardmin2  8707  infxpenlem  8719  alephgeom  8788  cardaleph  8795  infenaleph  8797  iscard3  8799  alephsson  8806  alephfp  8814  alephval3  8816  dfac12k  8852  axdc3lem2  9156  alephval2  9273  alephreg  9283  cfpwsdom  9285  alephom  9286  axrepndlem1  9293  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axpownd  9302  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  gchaleph2  9373  elwina  9387  elina  9388  winaon  9389  inawina  9391  winainf  9395  winalim  9396  tskr1om2  9469  r1tskina  9483  gruina  9519  grur1a  9520  indpi  9608  nqerrel  9633  recidnq  9666  ltaddnq  9675  pncan3  10168  divcan2  10572  ltp1  10740  ltm1  10742  recreclt  10801  elnn0z  11267  nn0ind-raph  11353  fzdifsuc  12270  2tnp1ge0ge0  12492  fsuppmapnn0fiubex  12654  faclbnd5  12947  hashfun  13084  ccatalpha  13228  2swrd2eqwrdeq  13544  caucvgrlem  14251  fsumcnv  14346  fprodcnv  14552  ef01bndlem  14753  sin01gt0  14759  cos01gt0  14760  egt2lt3  14773  cnso  14815  ltoddhalfle  14923  4sqlem12  15498  funcres  16379  fuchom  16444  xpsmnd  17153  xpsgrp  17357  mulgfval  17365  nmznsg  17461  symgplusg  17632  frgp0  17996  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  pwssplit1  18880  mvrf1  19246  blssioo  22406  dvidlem  23485  dvcj  23519  dvrec  23524  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  dv11cn  23568  dvivthlem2  23576  lhop1lem  23580  lhop1  23581  lhop2  23582  q1peqb  23718  pserdv  23987  sinhalfpilem  24019  tangtx  24061  efabl  24100  logneg2  24165  gausslemma2dlem1a  24890  lgseisenlem4  24903  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  dchrisum0lem3  25008  mulogsum  25021  pntrlog2bndlem1  25066  axlowdimlem7  25628  axlowdimlem10  25631  axcontlem6  25649  umgrbi  25767  constr3lem2  26174  el2spthonot0  26398  frisusgranb  26524  extwwlkfablem2  26605  hsn0elch  27489  axpjcl  27643  omlsilem  27645  pjchi  27675  shs00i  27693  chj00i  27730  chabs1  27759  pjspansn  27820  chscllem1  27880  osumcor2i  27887  nonbooli  27894  atcvat4i  28640  xppreima  28829  xdivrec  28966  psgndmfi  29177  sqsscirc1  29282  1stmbfm  29649  2ndmbfm  29650  carsgclctunlem2  29708  eulerpartlemgh  29767  bnj1148  30318  bnj1154  30321  cvmlift3lem5  30559  cvmlift3lem7  30561  logi  30873  dfon2lem3  30934  dfon2lem7  30938  distel  30953  altopthsn  31238  bj-exlimmpbi  32098  poimirlem9  32588  poimirlem26  32605  poimirlem27  32606  poimirlem32  32611  dvasin  32666  areacirclem4  32673  heiborlem8  32787  0rngo  32996  ax12eq  33244  ax12el  33245  ax12inda  33251  ax12v2-o  33252  nfded  33272  nfded2  33273  nfunidALT2  33274  lshpinN  33294  trlid0  34481  hdmap10lem  36149  islssfg2  36659  areaquad  36821  rnmptc  38348  fperdvper  38808  itgvol0  38860  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  wallispilem4  38961  dirkercncflem1  38996  dirkercncflem3  38998  dirkercncflem4  38999  fourierdlem35  39035  fourierdlem73  39072  lighneallem4b  40064  bgoldbwt  40199  sgoldbalt  40203  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  bgoldbtbndlem3  40223  rusgr1vtxlem  40787  31wlkond  41338  frcond3  41440  av-extwwlkfablem2  41510