Theorem impbida 560

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 113	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 113	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 127	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  eqrdav  2080  funfvbrb  5301  f1ocnv2d  5724  1stconst  5862  2ndconst  5863  cnvf1o  5866  ersymb  6143  swoer  6157  erth  6173  enen1  6334  enen2  6335  domen1  6336  domen2  6337  fidifsnen  6355  fundmfibi  6390  f1dmvrnfibi  6393  ordiso2  6446  fzsplit2  9069  fseq1p1m1  9111  elfz2nn0  9128  btwnzge0  9302  modqsubdir  9395  zesq  9591  rereb  9750  abslt  9974  absle  9975  maxleastb  10100  maxltsup  10104  iiserex  10177  dvdsadd2b  10242  nn0ob  10308  dfgcd3  10399  dfgcd2  10403  dvdsmulgcd  10414  lcmgcdeq  10465