Theorem impbida 586

Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)

Hypotheses

Ref	Expression
impbida.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
impbida.2	⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Assertion

Ref	Expression
impbida	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbida

Step	Hyp	Ref	Expression
1		impbida.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 114	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 114	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 128	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqrdav  2139  funfvbrb  5541  f1ocnv2d  5982  1stconst  6126  2ndconst  6127  cnvf1o  6130  ersymb  6451  swoer  6465  erth  6481  enen1  6742  enen2  6743  domen1  6744  domen2  6745  xpmapenlem  6751  fidifsnen  6772  fundmfibi  6835  f1dmvrnfibi  6840  ordiso2  6928  omniwomnimkv  7049  enwomnilem  7050  fzsplit2  9861  fseq1p1m1  9905  elfz2nn0  9923  btwnzge0  10104  modqsubdir  10197  zesq  10441  hashprg  10586  rereb  10667  abslt  10892  absle  10893  maxleastb  11018  maxltsup  11022  xrltmaxsup  11058  xrmaxltsup  11059  iserex  11140  mptfzshft  11243  fsumrev  11244  dvdsadd2b  11576  nn0ob  11641  dfgcd3  11734  dfgcd2  11738  dvdsmulgcd  11749  lcmgcdeq  11800  qden1elz  11919  cncnp  12438  xmetxpbl  12716  dedekindicc  12819  coseq0q4123  12963  coseq0negpitopi  12965  relogeftb  12994  relogbcxpbap  13090  pwf1oexmid  13367  isomninnlem  13400  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419  redcwlpolemeq1  13421