Theorem impbida 596

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqrdav  2176  funfvbrb  5626  f1ocnv2d  6070  1stconst  6217  2ndconst  6218  cnvf1o  6221  ersymb  6544  swoer  6558  erth  6574  enen1  6835  enen2  6836  domen1  6837  domen2  6838  xpmapenlem  6844  fidifsnen  6865  fundmfibi  6933  f1dmvrnfibi  6938  ordiso2  7029  omniwomnimkv  7160  enwomnilem  7162  nninfwlpoimlemginf  7169  exmidapne  7254  infregelbex  9592  fzsplit2  10043  fseq1p1m1  10087  elfz2nn0  10105  btwnzge0  10293  modqsubdir  10386  zesq  10631  hashprg  10779  rereb  10863  abslt  11088  absle  11089  maxleastb  11214  maxltsup  11218  xrltmaxsup  11256  xrmaxltsup  11257  iserex  11338  mptfzshft  11441  fsumrev  11442  fprodrev  11618  dvdsadd2b  11838  nn0ob  11903  dfgcd3  12001  dfgcd2  12005  dvdsmulgcd  12016  lcmgcdeq  12073  isprm5  12132  qden1elz  12195  issubmnd  12773  mhmf1o  12789  grpinvid1  12852  grpinvid2  12853  subsubg  12983  0unit  13197  cncnp  13512  xmetxpbl  13790  dedekindicc  13893  coseq0q4123  14037  coseq0negpitopi  14039  relogeftb  14068  relogbcxpbap  14165  pwf1oexmid  14520  isomninnlem  14549  apdiff  14567  iswomninnlem  14568  ismkvnnlem  14571  redcwlpolemeq1  14573