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  1idprl  6564  1idpru  6565  ltexprlemrnd  6577  ltaprg  6590  recexprlemrnd  6599  ltxrlt  6842  lttri3  6855  ltadd2  7172  reapti  7323  apreap  7331  ltmul1  7336  apreim  7347  ltleap  7373  mulap0b  7378  apmul1  7506  lt2msq  7593  nnsub  7693  zltnle  8027  zleloe  8028  zrevaddcl  8031  zltp1le  8034  zapne  8051  nn0n0n1ge2b  8056  zdiv  8064  nneo  8077  zeo2  8080  qrevaddcl  8313  xltneg  8479  iccid  8524  fzn  8636  0fz1  8639  uzsplit  8684  fzm1  8692  fzrevral  8697  ssfzo12bi  8811  frec2uzlt2d  8831  bj-notbi  9310