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  5756  f1ocnv2d  6222  1stconst  6381  2ndconst  6382  cnvf1o  6385  ersymb  6711  swoer  6725  erth  6743  pw2f1odclem  7015  enen1  7021  enen2  7022  domen1  7023  domen2  7024  xpmapenlem  7030  fidifsnen  7052  fundmfibi  7128  f1dmvrnfibi  7134  ordiso2  7225  omniwomnimkv  7357  enwomnilem  7359  nninfwlpoimlemginf  7366  pw1if  7433  exmidapne  7469  infregelbex  9822  fzsplit2  10275  fseq1p1m1  10319  elfz2nn0  10337  btwnzge0  10550  modqsubdir  10645  zesq  10910  hashprg  11062  rereb  11414  abslt  11639  absle  11640  maxleastb  11765  maxltsup  11769  xrltmaxsup  11808  xrmaxltsup  11809  iserex  11890  mptfzshft  11993  fsumrev  11994  fprodrev  12170  dvdsadd2b  12391  nn0ob  12459  bitsfzo  12506  dfgcd3  12571  dfgcd2  12575  dvdsmulgcd  12586  lcmgcdeq  12645  isprm5  12704  qden1elz  12767  issubmnd  13515  mhmf1o  13543  subsubm  13556  resmhm2b  13562  grpinvid1  13625  grpinvid2  13626  subsubg  13774  ssnmz  13788  ghmf1  13850  kerf1ghm  13851  ghmf1o  13852  conjnmzb  13857  0unit  14133  rhmf1o  14172  subsubrng  14218  subrgunit  14243  subsubrg  14249  islss3  14383  islss4  14386  lspsnel6  14412  lspsneq0b  14431  dflidl2rng  14485  cncnp  14944  xmetxpbl  15222  dedekindicc  15347  coseq0q4123  15548  coseq0negpitopi  15550  relogeftb  15579  relogbcxpbap  15679  upgr2wlkdc  16172  2omap  16530  pw1map  16532  pwf1oexmid  16536  isomninnlem  16570  apdiff  16588  iswomninnlem  16589  ismkvnnlem  16592  redcwlpolemeq1  16594