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  2204  funfvbrb  5693  f1ocnv2d  6150  1stconst  6307  2ndconst  6308  cnvf1o  6311  ersymb  6634  swoer  6648  erth  6666  pw2f1odclem  6931  enen1  6937  enen2  6938  domen1  6939  domen2  6940  xpmapenlem  6946  fidifsnen  6967  fundmfibi  7040  f1dmvrnfibi  7046  ordiso2  7137  omniwomnimkv  7269  enwomnilem  7271  nninfwlpoimlemginf  7278  exmidapne  7372  infregelbex  9719  fzsplit2  10172  fseq1p1m1  10216  elfz2nn0  10234  btwnzge0  10443  modqsubdir  10538  zesq  10803  hashprg  10953  rereb  11174  abslt  11399  absle  11400  maxleastb  11525  maxltsup  11529  xrltmaxsup  11568  xrmaxltsup  11569  iserex  11650  mptfzshft  11753  fsumrev  11754  fprodrev  11930  dvdsadd2b  12151  nn0ob  12219  bitsfzo  12266  dfgcd3  12331  dfgcd2  12335  dvdsmulgcd  12346  lcmgcdeq  12405  isprm5  12464  qden1elz  12527  issubmnd  13274  mhmf1o  13302  subsubm  13315  resmhm2b  13321  grpinvid1  13384  grpinvid2  13385  subsubg  13533  ssnmz  13547  ghmf1  13609  kerf1ghm  13610  ghmf1o  13611  conjnmzb  13616  0unit  13891  rhmf1o  13930  subsubrng  13976  subrgunit  14001  subsubrg  14007  islss3  14141  islss4  14144  lspsnel6  14170  lspsneq0b  14189  dflidl2rng  14243  cncnp  14702  xmetxpbl  14980  dedekindicc  15105  coseq0q4123  15306  coseq0negpitopi  15308  relogeftb  15337  relogbcxpbap  15437  2omap  15932  pwf1oexmid  15936  isomninnlem  15969  apdiff  15987  iswomninnlem  15988  ismkvnnlem  15991  redcwlpolemeq1  15993