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  6226  1stconst  6385  2ndconst  6386  cnvf1o  6389  ersymb  6715  swoer  6729  erth  6747  pw2f1odclem  7019  enen1  7025  enen2  7026  domen1  7027  domen2  7028  xpmapenlem  7034  fidifsnen  7056  fundmfibi  7136  f1dmvrnfibi  7142  ordiso2  7233  omniwomnimkv  7365  enwomnilem  7367  nninfwlpoimlemginf  7374  pw1if  7442  exmidapne  7478  infregelbex  9831  fzsplit2  10284  fseq1p1m1  10328  elfz2nn0  10346  btwnzge0  10559  modqsubdir  10654  zesq  10919  hashprg  11071  rereb  11423  abslt  11648  absle  11649  maxleastb  11774  maxltsup  11778  xrltmaxsup  11817  xrmaxltsup  11818  iserex  11899  mptfzshft  12002  fsumrev  12003  fprodrev  12179  dvdsadd2b  12400  nn0ob  12468  bitsfzo  12515  dfgcd3  12580  dfgcd2  12584  dvdsmulgcd  12595  lcmgcdeq  12654  isprm5  12713  qden1elz  12776  issubmnd  13524  mhmf1o  13552  subsubm  13565  resmhm2b  13571  grpinvid1  13634  grpinvid2  13635  subsubg  13783  ssnmz  13797  ghmf1  13859  kerf1ghm  13860  ghmf1o  13861  conjnmzb  13866  0unit  14142  rhmf1o  14181  subsubrng  14227  subrgunit  14252  subsubrg  14258  islss3  14392  islss4  14395  lspsnel6  14421  lspsneq0b  14440  dflidl2rng  14494  cncnp  14953  xmetxpbl  15231  dedekindicc  15356  coseq0q4123  15557  coseq0negpitopi  15559  relogeftb  15588  relogbcxpbap  15688  upgr2wlkdc  16227  2omap  16594  pw1map  16596  pwf1oexmid  16600  isomninnlem  16634  apdiff  16652  iswomninnlem  16653  ismkvnnlem  16656  redcwlpolemeq1  16658