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  5750  f1ocnv2d  6216  1stconst  6373  2ndconst  6374  cnvf1o  6377  ersymb  6702  swoer  6716  erth  6734  pw2f1odclem  7003  enen1  7009  enen2  7010  domen1  7011  domen2  7012  xpmapenlem  7018  fidifsnen  7040  fundmfibi  7116  f1dmvrnfibi  7122  ordiso2  7213  omniwomnimkv  7345  enwomnilem  7347  nninfwlpoimlemginf  7354  pw1if  7421  exmidapne  7457  infregelbex  9805  fzsplit2  10258  fseq1p1m1  10302  elfz2nn0  10320  btwnzge0  10532  modqsubdir  10627  zesq  10892  hashprg  11043  rereb  11389  abslt  11614  absle  11615  maxleastb  11740  maxltsup  11744  xrltmaxsup  11783  xrmaxltsup  11784  iserex  11865  mptfzshft  11968  fsumrev  11969  fprodrev  12145  dvdsadd2b  12366  nn0ob  12434  bitsfzo  12481  dfgcd3  12546  dfgcd2  12550  dvdsmulgcd  12561  lcmgcdeq  12620  isprm5  12679  qden1elz  12742  issubmnd  13490  mhmf1o  13518  subsubm  13531  resmhm2b  13537  grpinvid1  13600  grpinvid2  13601  subsubg  13749  ssnmz  13763  ghmf1  13825  kerf1ghm  13826  ghmf1o  13827  conjnmzb  13832  0unit  14108  rhmf1o  14147  subsubrng  14193  subrgunit  14218  subsubrg  14224  islss3  14358  islss4  14361  lspsnel6  14387  lspsneq0b  14406  dflidl2rng  14460  cncnp  14919  xmetxpbl  15197  dedekindicc  15322  coseq0q4123  15523  coseq0negpitopi  15525  relogeftb  15554  relogbcxpbap  15654  upgr2wlkdc  16116  2omap  16418  pw1map  16420  pwf1oexmid  16424  isomninnlem  16458  apdiff  16476  iswomninnlem  16477  ismkvnnlem  16480  redcwlpolemeq1  16482