Theorem impbida 598

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  616  eqrdav  2228  funfvbrb  5747  f1ocnv2d  6208  1stconst  6365  2ndconst  6366  cnvf1o  6369  ersymb  6692  swoer  6706  erth  6724  pw2f1odclem  6991  enen1  6997  enen2  6998  domen1  6999  domen2  7000  xpmapenlem  7006  fidifsnen  7028  fundmfibi  7101  f1dmvrnfibi  7107  ordiso2  7198  omniwomnimkv  7330  enwomnilem  7332  nninfwlpoimlemginf  7339  pw1if  7406  exmidapne  7442  infregelbex  9789  fzsplit2  10242  fseq1p1m1  10286  elfz2nn0  10304  btwnzge0  10515  modqsubdir  10610  zesq  10875  hashprg  11025  rereb  11369  abslt  11594  absle  11595  maxleastb  11720  maxltsup  11724  xrltmaxsup  11763  xrmaxltsup  11764  iserex  11845  mptfzshft  11948  fsumrev  11949  fprodrev  12125  dvdsadd2b  12346  nn0ob  12414  bitsfzo  12461  dfgcd3  12526  dfgcd2  12530  dvdsmulgcd  12541  lcmgcdeq  12600  isprm5  12659  qden1elz  12722  issubmnd  13470  mhmf1o  13498  subsubm  13511  resmhm2b  13517  grpinvid1  13580  grpinvid2  13581  subsubg  13729  ssnmz  13743  ghmf1  13805  kerf1ghm  13806  ghmf1o  13807  conjnmzb  13812  0unit  14087  rhmf1o  14126  subsubrng  14172  subrgunit  14197  subsubrg  14203  islss3  14337  islss4  14340  lspsnel6  14366  lspsneq0b  14385  dflidl2rng  14439  cncnp  14898  xmetxpbl  15176  dedekindicc  15301  coseq0q4123  15502  coseq0negpitopi  15504  relogeftb  15533  relogbcxpbap  15633  2omap  16318  pw1map  16320  pwf1oexmid  16324  isomninnlem  16357  apdiff  16375  iswomninnlem  16376  ismkvnnlem  16379  redcwlpolemeq1  16381