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  2206  funfvbrb  5716  f1ocnv2d  6173  1stconst  6330  2ndconst  6331  cnvf1o  6334  ersymb  6657  swoer  6671  erth  6689  pw2f1odclem  6956  enen1  6962  enen2  6963  domen1  6964  domen2  6965  xpmapenlem  6971  fidifsnen  6993  fundmfibi  7066  f1dmvrnfibi  7072  ordiso2  7163  omniwomnimkv  7295  enwomnilem  7297  nninfwlpoimlemginf  7304  pw1if  7371  exmidapne  7407  infregelbex  9754  fzsplit2  10207  fseq1p1m1  10251  elfz2nn0  10269  btwnzge0  10480  modqsubdir  10575  zesq  10840  hashprg  10990  rereb  11289  abslt  11514  absle  11515  maxleastb  11640  maxltsup  11644  xrltmaxsup  11683  xrmaxltsup  11684  iserex  11765  mptfzshft  11868  fsumrev  11869  fprodrev  12045  dvdsadd2b  12266  nn0ob  12334  bitsfzo  12381  dfgcd3  12446  dfgcd2  12450  dvdsmulgcd  12461  lcmgcdeq  12520  isprm5  12579  qden1elz  12642  issubmnd  13389  mhmf1o  13417  subsubm  13430  resmhm2b  13436  grpinvid1  13499  grpinvid2  13500  subsubg  13648  ssnmz  13662  ghmf1  13724  kerf1ghm  13725  ghmf1o  13726  conjnmzb  13731  0unit  14006  rhmf1o  14045  subsubrng  14091  subrgunit  14116  subsubrg  14122  islss3  14256  islss4  14259  lspsnel6  14285  lspsneq0b  14304  dflidl2rng  14358  cncnp  14817  xmetxpbl  15095  dedekindicc  15220  coseq0q4123  15421  coseq0negpitopi  15423  relogeftb  15452  relogbcxpbap  15552  2omap  16132  pw1map  16134  pwf1oexmid  16138  isomninnlem  16171  apdiff  16189  iswomninnlem  16190  ismkvnnlem  16193  redcwlpolemeq1  16195