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  2195  funfvbrb  5678  f1ocnv2d  6131  1stconst  6288  2ndconst  6289  cnvf1o  6292  ersymb  6615  swoer  6629  erth  6647  pw2f1odclem  6904  enen1  6910  enen2  6911  domen1  6912  domen2  6913  xpmapenlem  6919  fidifsnen  6940  fundmfibi  7013  f1dmvrnfibi  7019  ordiso2  7110  omniwomnimkv  7242  enwomnilem  7244  nninfwlpoimlemginf  7251  exmidapne  7345  infregelbex  9691  fzsplit2  10144  fseq1p1m1  10188  elfz2nn0  10206  btwnzge0  10409  modqsubdir  10504  zesq  10769  hashprg  10919  rereb  11047  abslt  11272  absle  11273  maxleastb  11398  maxltsup  11402  xrltmaxsup  11441  xrmaxltsup  11442  iserex  11523  mptfzshft  11626  fsumrev  11627  fprodrev  11803  dvdsadd2b  12024  nn0ob  12092  bitsfzo  12139  dfgcd3  12204  dfgcd2  12208  dvdsmulgcd  12219  lcmgcdeq  12278  isprm5  12337  qden1elz  12400  issubmnd  13146  mhmf1o  13174  subsubm  13187  resmhm2b  13193  grpinvid1  13256  grpinvid2  13257  subsubg  13405  ssnmz  13419  ghmf1  13481  kerf1ghm  13482  ghmf1o  13483  conjnmzb  13488  0unit  13763  rhmf1o  13802  subsubrng  13848  subrgunit  13873  subsubrg  13879  islss3  14013  islss4  14016  lspsnel6  14042  lspsneq0b  14061  dflidl2rng  14115  cncnp  14574  xmetxpbl  14852  dedekindicc  14977  coseq0q4123  15178  coseq0negpitopi  15180  relogeftb  15209  relogbcxpbap  15309  2omap  15750  pwf1oexmid  15754  isomninnlem  15787  apdiff  15805  iswomninnlem  15806  ismkvnnlem  15809  redcwlpolemeq1  15811