Theorem impbida 600

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  618  eqrdav  2230  funfvbrb  5760  f1ocnv2d  6227  1stconst  6386  2ndconst  6387  cnvf1o  6390  ersymb  6716  swoer  6730  erth  6748  pw2f1odclem  7020  enen1  7026  enen2  7027  domen1  7028  domen2  7029  xpmapenlem  7035  fidifsnen  7057  fundmfibi  7137  f1dmvrnfibi  7143  ordiso2  7234  omniwomnimkv  7366  enwomnilem  7368  nninfwlpoimlemginf  7375  pw1if  7443  exmidapne  7479  infregelbex  9832  fzsplit2  10285  fseq1p1m1  10329  elfz2nn0  10347  btwnzge0  10561  modqsubdir  10656  zesq  10921  hashprg  11073  rereb  11428  abslt  11653  absle  11654  maxleastb  11779  maxltsup  11783  xrltmaxsup  11822  xrmaxltsup  11823  iserex  11904  mptfzshft  12008  fsumrev  12009  fprodrev  12185  dvdsadd2b  12406  nn0ob  12474  bitsfzo  12521  dfgcd3  12586  dfgcd2  12590  dvdsmulgcd  12601  lcmgcdeq  12660  isprm5  12719  qden1elz  12782  issubmnd  13530  mhmf1o  13558  subsubm  13571  resmhm2b  13577  grpinvid1  13640  grpinvid2  13641  subsubg  13789  ssnmz  13803  ghmf1  13865  kerf1ghm  13866  ghmf1o  13867  conjnmzb  13872  0unit  14149  rhmf1o  14188  subsubrng  14234  subrgunit  14259  subsubrg  14265  islss3  14399  islss4  14402  lspsnel6  14428  lspsneq0b  14447  dflidl2rng  14501  cncnp  14960  xmetxpbl  15238  dedekindicc  15363  coseq0q4123  15564  coseq0negpitopi  15566  relogeftb  15595  relogbcxpbap  15695  upgr2wlkdc  16234  2omap  16620  pw1map  16622  pwf1oexmid  16626  isomninnlem  16660  apdiff  16678  iswomninnlem  16680  ismkvnnlem  16683  redcwlpolemeq1  16685