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  2156  funfvbrb  5580  f1ocnv2d  6024  1stconst  6168  2ndconst  6169  cnvf1o  6172  ersymb  6494  swoer  6508  erth  6524  enen1  6785  enen2  6786  domen1  6787  domen2  6788  xpmapenlem  6794  fidifsnen  6815  fundmfibi  6883  f1dmvrnfibi  6888  ordiso2  6979  omniwomnimkv  7110  enwomnilem  7112  infregelbex  9509  fzsplit2  9952  fseq1p1m1  9996  elfz2nn0  10014  btwnzge0  10199  modqsubdir  10292  zesq  10536  hashprg  10682  rereb  10763  abslt  10988  absle  10989  maxleastb  11114  maxltsup  11118  xrltmaxsup  11154  xrmaxltsup  11155  iserex  11236  mptfzshft  11339  fsumrev  11340  fprodrev  11516  dvdsadd2b  11733  nn0ob  11798  dfgcd3  11893  dfgcd2  11897  dvdsmulgcd  11908  lcmgcdeq  11959  qden1elz  12079  cncnp  12630  xmetxpbl  12908  dedekindicc  13011  coseq0q4123  13155  coseq0negpitopi  13157  relogeftb  13186  relogbcxpbap  13282  pwf1oexmid  13571  isomninnlem  13601  apdiff  13619  iswomninnlem  13620  ismkvnnlem  13623  redcwlpolemeq1  13625