Theorem impbida 585

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  2136  funfvbrb  5526  f1ocnv2d  5967  1stconst  6111  2ndconst  6112  cnvf1o  6115  ersymb  6436  swoer  6450  erth  6466  enen1  6727  enen2  6728  domen1  6729  domen2  6730  xpmapenlem  6736  fidifsnen  6757  fundmfibi  6820  f1dmvrnfibi  6825  ordiso2  6913  fzsplit2  9823  fseq1p1m1  9867  elfz2nn0  9885  btwnzge0  10066  modqsubdir  10159  zesq  10403  hashprg  10547  rereb  10628  abslt  10853  absle  10854  maxleastb  10979  maxltsup  10983  xrltmaxsup  11019  xrmaxltsup  11020  iserex  11101  mptfzshft  11204  fsumrev  11205  dvdsadd2b  11529  nn0ob  11594  dfgcd3  11687  dfgcd2  11691  dvdsmulgcd  11702  lcmgcdeq  11753  qden1elz  11872  cncnp  12388  xmetxpbl  12666  dedekindicc  12769  coseq0q4123  12904  coseq0negpitopi  12906  pwf1oexmid  13183  isomninnlem  13214