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  5769  f1ocnv2d  6237  1stconst  6395  2ndconst  6396  cnvf1o  6399  ersymb  6759  swoer  6773  erth  6791  pw2f1odclem  7063  enen1  7069  enen2  7070  domen1  7071  domen2  7072  xpmapenlem  7078  fidifsnen  7100  fundmfibi  7180  f1dmvrnfibi  7186  ordiso2  7277  omniwomnimkv  7409  enwomnilem  7411  nninfwlpoimlemginf  7418  pw1if  7486  exmidapne  7522  infregelbex  9876  fzsplit2  10330  fseq1p1m1  10374  elfz2nn0  10392  btwnzge0  10606  modqsubdir  10701  zesq  10966  hashprg  11118  rereb  11486  abslt  11711  absle  11712  maxleastb  11837  maxltsup  11841  xrltmaxsup  11880  xrmaxltsup  11881  iserex  11962  mptfzshft  12066  fsumrev  12067  fprodrev  12243  dvdsadd2b  12464  nn0ob  12532  bitsfzo  12579  dfgcd3  12644  dfgcd2  12648  dvdsmulgcd  12659  lcmgcdeq  12718  isprm5  12777  qden1elz  12840  issubmnd  13588  mhmf1o  13616  subsubm  13629  resmhm2b  13635  grpinvid1  13698  grpinvid2  13699  subsubg  13847  ssnmz  13861  ghmf1  13923  kerf1ghm  13924  ghmf1o  13925  conjnmzb  13930  0unit  14207  rhmf1o  14246  subsubrng  14292  subrgunit  14317  subsubrg  14323  islss3  14458  islss4  14461  lspsnel6  14487  lspsneq0b  14506  dflidl2rng  14560  cncnp  15024  xmetxpbl  15302  dedekindicc  15427  coseq0q4123  15628  coseq0negpitopi  15630  relogeftb  15659  relogbcxpbap  15759  upgr2wlkdc  16301  2omap  16698  pw1map  16700  pwf1oexmid  16704  isomninnlem  16745  apdiff  16763  iswomninnlem  16765  ismkvnnlem  16768  redcwlpolemeq1  16770