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  2203  funfvbrb  5692  f1ocnv2d  6149  1stconst  6306  2ndconst  6307  cnvf1o  6310  ersymb  6633  swoer  6647  erth  6665  pw2f1odclem  6930  enen1  6936  enen2  6937  domen1  6938  domen2  6939  xpmapenlem  6945  fidifsnen  6966  fundmfibi  7039  f1dmvrnfibi  7045  ordiso2  7136  omniwomnimkv  7268  enwomnilem  7270  nninfwlpoimlemginf  7277  exmidapne  7371  infregelbex  9718  fzsplit2  10171  fseq1p1m1  10215  elfz2nn0  10233  btwnzge0  10441  modqsubdir  10536  zesq  10801  hashprg  10951  rereb  11145  abslt  11370  absle  11371  maxleastb  11496  maxltsup  11500  xrltmaxsup  11539  xrmaxltsup  11540  iserex  11621  mptfzshft  11724  fsumrev  11725  fprodrev  11901  dvdsadd2b  12122  nn0ob  12190  bitsfzo  12237  dfgcd3  12302  dfgcd2  12306  dvdsmulgcd  12317  lcmgcdeq  12376  isprm5  12435  qden1elz  12498  issubmnd  13245  mhmf1o  13273  subsubm  13286  resmhm2b  13292  grpinvid1  13355  grpinvid2  13356  subsubg  13504  ssnmz  13518  ghmf1  13580  kerf1ghm  13581  ghmf1o  13582  conjnmzb  13587  0unit  13862  rhmf1o  13901  subsubrng  13947  subrgunit  13972  subsubrg  13978  islss3  14112  islss4  14115  lspsnel6  14141  lspsneq0b  14160  dflidl2rng  14214  cncnp  14673  xmetxpbl  14951  dedekindicc  15076  coseq0q4123  15277  coseq0negpitopi  15279  relogeftb  15308  relogbcxpbap  15408  2omap  15894  pwf1oexmid  15898  isomninnlem  15931  apdiff  15949  iswomninnlem  15950  ismkvnnlem  15953  redcwlpolemeq1  15955