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  2231  funfvbrb  5791  f1ocnv2d  6259  1stconst  6417  2ndconst  6418  cnvf1o  6421  ersymb  6781  swoer  6795  erth  6813  pw2f1odclem  7087  enen1  7093  enen2  7094  domen1  7095  domen2  7096  xpmapenlem  7102  fidifsnen  7125  fundmfibi  7205  f1dmvrnfibi  7211  2omap  7269  2omapfi  7271  ordiso2  7326  omniwomnimkv  7458  enwomnilem  7460  nninfwlpoimlemginf  7467  pw1if  7535  exmidapne  7574  infregelbex  9930  fzsplit2  10384  fseq1p1m1  10428  elfz2nn0  10446  btwnzge0  10660  modqsubdir  10755  zesq  11020  hashprg  11173  sseqn  11203  hashfibclem  11206  rereb  11548  abslt  11773  absle  11774  maxleastb  11899  maxltsup  11903  xrltmaxsup  11942  xrmaxltsup  11943  iserex  12024  mptfzshft  12128  fsumrev  12129  fprodrev  12305  dvdsadd2b  12526  nn0ob  12594  bitsfzo  12641  dfgcd3  12706  dfgcd2  12710  dvdsmulgcd  12721  lcmgcdeq  12780  isprm5  12839  qden1elz  12902  issubmnd  13655  mhmf1o  13683  subsubm  13696  resmhm2b  13702  grpinvid1  13765  grpinvid2  13766  subsubg  13914  ssnmz  13928  ghmf1  13990  kerf1ghm  13991  ghmf1o  13992  conjnmzb  13997  0unit  14274  rhmf1o  14313  subsubrng  14359  subrgunit  14384  subsubrg  14390  islss3  14527  islss4  14530  lspsnel6  14556  lspsneq0b  14575  dflidl2rng  14629  cncnp  15095  xmetxpbl  15373  dedekindicc  15498  coseq0q4123  15699  coseq0negpitopi  15701  relogeftb  15730  relogbcxpbap  15830  upgr2wlkdc  16372  pw1map  16769  pwf1oexmid  16773  isomninnlem  16814  apdiff  16832  iswomninnlem  16834  ismkvnnlem  16837  redcwlpolemeq1  16839