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  6504  genprndu  6505  nqprl  6533  1idprl  6566  1idpru  6567  ltexprlemrnd  6579  ltaprg  6592  recexprlemrnd  6601  cauappcvgprlemrnd  6622  caucvgprlemrnd  6644  ltxrlt  6882  lttri3  6895  ltadd2  7212  reapti  7363  apreap  7371  ltmul1  7376  apreim  7387  ltleap  7413  mulap0b  7418  apmul1  7546  lt2msq  7633  nnsub  7733  zltnle  8067  zleloe  8068  zrevaddcl  8071  zltp1le  8074  zapne  8091  nn0n0n1ge2b  8096  zdiv  8104  nneo  8117  zeo2  8120  qrevaddcl  8353  xltneg  8519  iccid  8564  fzn  8676  0fz1  8679  uzsplit  8724  fzm1  8732  fzrevral  8737  ssfzo12bi  8851  frec2uzlt2d  8871  sqrtsq  9214  bj-notbi  9380