Theorem impbida 600

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  618  eqrdav  2230  funfvbrb  5760  f1ocnv2d  6227  1stconst  6386  2ndconst  6387  cnvf1o  6390  ersymb  6716  swoer  6730  erth  6748  pw2f1odclem  7020  enen1  7026  enen2  7027  domen1  7028  domen2  7029  xpmapenlem  7035  fidifsnen  7057  fundmfibi  7137  f1dmvrnfibi  7143  ordiso2  7234  omniwomnimkv  7366  enwomnilem  7368  nninfwlpoimlemginf  7375  pw1if  7443  exmidapne  7479  infregelbex  9832  fzsplit2  10285  fseq1p1m1  10329  elfz2nn0  10347  btwnzge0  10560  modqsubdir  10655  zesq  10920  hashprg  11072  rereb  11424  abslt  11649  absle  11650  maxleastb  11775  maxltsup  11779  xrltmaxsup  11818  xrmaxltsup  11819  iserex  11900  mptfzshft  12004  fsumrev  12005  fprodrev  12181  dvdsadd2b  12402  nn0ob  12470  bitsfzo  12517  dfgcd3  12582  dfgcd2  12586  dvdsmulgcd  12597  lcmgcdeq  12656  isprm5  12715  qden1elz  12778  issubmnd  13526  mhmf1o  13554  subsubm  13567  resmhm2b  13573  grpinvid1  13636  grpinvid2  13637  subsubg  13785  ssnmz  13799  ghmf1  13861  kerf1ghm  13862  ghmf1o  13863  conjnmzb  13868  0unit  14145  rhmf1o  14184  subsubrng  14230  subrgunit  14255  subsubrg  14261  islss3  14395  islss4  14398  lspsnel6  14424  lspsneq0b  14443  dflidl2rng  14497  cncnp  14956  xmetxpbl  15234  dedekindicc  15359  coseq0q4123  15560  coseq0negpitopi  15562  relogeftb  15591  relogbcxpbap  15691  upgr2wlkdc  16230  2omap  16597  pw1map  16599  pwf1oexmid  16603  isomninnlem  16637  apdiff  16655  iswomninnlem  16656  ismkvnnlem  16659  redcwlpolemeq1  16661