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  5629  f1ocnv2d  6074  1stconst  6221  2ndconst  6222  cnvf1o  6225  ersymb  6548  swoer  6562  erth  6578  enen1  6839  enen2  6840  domen1  6841  domen2  6842  xpmapenlem  6848  fidifsnen  6869  fundmfibi  6937  f1dmvrnfibi  6942  ordiso2  7033  omniwomnimkv  7164  enwomnilem  7166  nninfwlpoimlemginf  7173  exmidapne  7258  infregelbex  9597  fzsplit2  10049  fseq1p1m1  10093  elfz2nn0  10111  btwnzge0  10299  modqsubdir  10392  zesq  10638  hashprg  10787  rereb  10871  abslt  11096  absle  11097  maxleastb  11222  maxltsup  11226  xrltmaxsup  11264  xrmaxltsup  11265  iserex  11346  mptfzshft  11449  fsumrev  11450  fprodrev  11626  dvdsadd2b  11846  nn0ob  11912  dfgcd3  12010  dfgcd2  12014  dvdsmulgcd  12025  lcmgcdeq  12082  isprm5  12141  qden1elz  12204  issubmnd  12842  mhmf1o  12860  grpinvid1  12923  grpinvid2  12924  subsubg  13055  ssnmz  13069  0unit  13296  subrgunit  13358  subsubrg  13364  cncnp  13700  xmetxpbl  13978  dedekindicc  14081  coseq0q4123  14225  coseq0negpitopi  14227  relogeftb  14256  relogbcxpbap  14353  pwf1oexmid  14719  isomninnlem  14748  apdiff  14766  iswomninnlem  14767  ismkvnnlem  14770  redcwlpolemeq1  14772