Theorem impbid 120

Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

Ref	Expression
impbid.1	⊢ (φ → (ψ → χ))
impbid.2	⊢ (φ → (χ → ψ))

Assertion

Ref	Expression
impbid	⊢ (φ → (ψ ↔ χ))

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 ⊢ (φ → (ψ → χ))
2		impbid.2	. . 3 ⊢ (φ → (χ → ψ))
3	1, 2	impbid21d 119	. 2 ⊢ (φ → (φ → (ψ ↔ χ)))
4	3	pm2.43i 43	1 ⊢ (φ → (ψ ↔ χ))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicom1  122  impbid1  130  pm5.74  168  imbi1d  220  pm5.501  233  pm5.32d  423  impbida  528  notbid  591  pm5.21  610  nbn2  612  2falsed  617  pm5.21ndd  620  orbi2d  703  con4biddc  753  con1bidc  767  con1bdc  771  oibabs  799  dedlema  875  dedlemb  876  xorbin  1272  albi  1354  19.21ht  1470  exbi  1492  19.23t  1564  equequ1  1595  equequ2  1596  elequ1  1597  elequ2  1598  equsexd  1614  dral1  1615  cbv2h  1631  sbequ12  1651  sbiedh  1667  drex1  1676  ax11b  1704  sbequ  1718  sbft  1725  sb56  1762  cbvexdh  1798  eupickb  1978  eupickbi  1979  ceqsalt  2574  ceqex  2665  mob2  2715  euxfr2dc  2720  reu6  2724  sbciegft  2787  eqsbc3r  2813  csbiebt  2880  sseq1  2960  reupick  3215  reupick2  3217  disjeq2  3740  disjeq1  3743  copsexg  3972  euotd  3982  poeq2  4028  sotritric  4052  sotritrieq  4053  seeq1  4061  seeq2  4062  alxfr  4159  ralxfrd  4160  rexxfrd  4161  ordelsuc  4197  sosng  4356  iss  4597  iotaval  4821  funeq  4864  funssres  4885  tz6.12c  5146  fnbrfvb  5157  ssimaex  5177  fvimacnv  5225  elpreima  5229  fsn  5278  fconst2g  5319  elunirn  5348  f1ocnvfvb  5363  foeqcnvco  5373  f1eqcocnv  5374  fliftfun  5379  isose  5403  isopo  5405  isoso  5407  f1oiso2  5409  eusvobj2  5441  oprabid  5480  f1opw2  5648  op1steq  5747  rntpos  5813  nnsucelsuc  6009  nnsucsssuc  6010  nnaord  6018  nnmord  6026  nnaordex  6036  nnawordex  6037  nnm00  6038  erexb  6067  swoord1  6071  swoord2  6072  iinerm  6114  fundmen  6222  ltexnqq  6391  genprndl  6503  genprndu  6504  nqprl  6532  1idprl  6565  1idpru  6566  ltexprlemrnd  6578  ltaprg  6591  recexprlemrnd  6600  cauappcvgprlemrnd  6621  ltxrlt  6862  lttri3  6875  ltadd2  7192  reapti  7343  apreap  7351  ltmul1  7356  apreim  7367  ltleap  7393  mulap0b  7398  apmul1  7526  lt2msq  7613  nnsub  7713  zltnle  8047  zleloe  8048  zrevaddcl  8051  zltp1le  8054  zapne  8071  nn0n0n1ge2b  8076  zdiv  8084  nneo  8097  zeo2  8100  qrevaddcl  8333  xltneg  8499  iccid  8544  fzn  8656  0fz1  8659  uzsplit  8704  fzm1  8712  fzrevral  8717  ssfzo12bi  8831  frec2uzlt2d  8851  sqrtsq  9194  bj-notbi  9356