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:  biadanid  614  eqrdav  2195  funfvbrb  5678  f1ocnv2d  6131  1stconst  6288  2ndconst  6289  cnvf1o  6292  ersymb  6615  swoer  6629  erth  6647  pw2f1odclem  6904  enen1  6910  enen2  6911  domen1  6912  domen2  6913  xpmapenlem  6919  fidifsnen  6940  fundmfibi  7013  f1dmvrnfibi  7019  ordiso2  7110  omniwomnimkv  7242  enwomnilem  7244  nninfwlpoimlemginf  7251  exmidapne  7343  infregelbex  9689  fzsplit2  10142  fseq1p1m1  10186  elfz2nn0  10204  btwnzge0  10407  modqsubdir  10502  zesq  10767  hashprg  10917  rereb  11045  abslt  11270  absle  11271  maxleastb  11396  maxltsup  11400  xrltmaxsup  11439  xrmaxltsup  11440  iserex  11521  mptfzshft  11624  fsumrev  11625  fprodrev  11801  dvdsadd2b  12022  nn0ob  12090  bitsfzo  12137  dfgcd3  12202  dfgcd2  12206  dvdsmulgcd  12217  lcmgcdeq  12276  isprm5  12335  qden1elz  12398  issubmnd  13144  mhmf1o  13172  subsubm  13185  resmhm2b  13191  grpinvid1  13254  grpinvid2  13255  subsubg  13403  ssnmz  13417  ghmf1  13479  kerf1ghm  13480  ghmf1o  13481  conjnmzb  13486  0unit  13761  rhmf1o  13800  subsubrng  13846  subrgunit  13871  subsubrg  13877  islss3  14011  islss4  14014  lspsnel6  14040  lspsneq0b  14059  dflidl2rng  14113  cncnp  14550  xmetxpbl  14828  dedekindicc  14953  coseq0q4123  15154  coseq0negpitopi  15156  relogeftb  15185  relogbcxpbap  15285  2omap  15726  pwf1oexmid  15730  isomninnlem  15761  apdiff  15779  iswomninnlem  15780  ismkvnnlem  15783  redcwlpolemeq1  15785