Theorem impbida 564

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-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqrdav  2094  funfvbrb  5451  f1ocnv2d  5886  1stconst  6024  2ndconst  6025  cnvf1o  6028  ersymb  6346  swoer  6360  erth  6376  enen1  6636  enen2  6637  domen1  6638  domen2  6639  xpmapenlem  6645  fidifsnen  6666  fundmfibi  6728  f1dmvrnfibi  6733  ordiso2  6808  fzsplit2  9613  fseq1p1m1  9657  elfz2nn0  9675  btwnzge0  9856  modqsubdir  9949  zesq  10187  hashprg  10331  rereb  10412  abslt  10636  absle  10637  maxleastb  10762  maxltsup  10766  xrltmaxsup  10800  xrmaxltsup  10801  iserex  10882  mptfzshft  10985  fsumrev  10986  dvdsadd2b  11270  nn0ob  11335  dfgcd3  11426  dfgcd2  11430  dvdsmulgcd  11441  lcmgcdeq  11492  qden1elz  11610  cncnp  12081