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  5630  f1ocnv2d  6075  1stconst  6222  2ndconst  6223  cnvf1o  6226  ersymb  6549  swoer  6563  erth  6579  enen1  6840  enen2  6841  domen1  6842  domen2  6843  xpmapenlem  6849  fidifsnen  6870  fundmfibi  6938  f1dmvrnfibi  6943  ordiso2  7034  omniwomnimkv  7165  enwomnilem  7167  nninfwlpoimlemginf  7174  exmidapne  7259  infregelbex  9598  fzsplit2  10050  fseq1p1m1  10094  elfz2nn0  10112  btwnzge0  10300  modqsubdir  10393  zesq  10639  hashprg  10788  rereb  10872  abslt  11097  absle  11098  maxleastb  11223  maxltsup  11227  xrltmaxsup  11265  xrmaxltsup  11266  iserex  11347  mptfzshft  11450  fsumrev  11451  fprodrev  11627  dvdsadd2b  11847  nn0ob  11913  dfgcd3  12011  dfgcd2  12015  dvdsmulgcd  12026  lcmgcdeq  12083  isprm5  12142  qden1elz  12205  issubmnd  12843  mhmf1o  12861  grpinvid1  12924  grpinvid2  12925  subsubg  13057  ssnmz  13071  0unit  13298  subrgunit  13360  subsubrg  13366  cncnp  13733  xmetxpbl  14011  dedekindicc  14114  coseq0q4123  14258  coseq0negpitopi  14260  relogeftb  14289  relogbcxpbap  14386  pwf1oexmid  14752  isomninnlem  14781  apdiff  14799  iswomninnlem  14800  ismkvnnlem  14803  redcwlpolemeq1  14805