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  2192  funfvbrb  5672  f1ocnv2d  6124  1stconst  6276  2ndconst  6277  cnvf1o  6280  ersymb  6603  swoer  6617  erth  6635  pw2f1odclem  6892  enen1  6898  enen2  6899  domen1  6900  domen2  6901  xpmapenlem  6907  fidifsnen  6928  fundmfibi  6999  f1dmvrnfibi  7005  ordiso2  7096  omniwomnimkv  7228  enwomnilem  7230  nninfwlpoimlemginf  7237  exmidapne  7322  infregelbex  9666  fzsplit2  10119  fseq1p1m1  10163  elfz2nn0  10181  btwnzge0  10372  modqsubdir  10467  zesq  10732  hashprg  10882  rereb  11010  abslt  11235  absle  11236  maxleastb  11361  maxltsup  11365  xrltmaxsup  11403  xrmaxltsup  11404  iserex  11485  mptfzshft  11588  fsumrev  11589  fprodrev  11765  dvdsadd2b  11986  nn0ob  12052  dfgcd3  12150  dfgcd2  12154  dvdsmulgcd  12165  lcmgcdeq  12224  isprm5  12283  qden1elz  12346  issubmnd  13026  mhmf1o  13045  subsubm  13058  resmhm2b  13064  grpinvid1  13127  grpinvid2  13128  subsubg  13270  ssnmz  13284  ghmf1  13346  kerf1ghm  13347  ghmf1o  13348  conjnmzb  13353  0unit  13628  rhmf1o  13667  subsubrng  13713  subrgunit  13738  subsubrg  13744  islss3  13878  islss4  13881  lspsnel6  13907  lspsneq0b  13926  dflidl2rng  13980  cncnp  14409  xmetxpbl  14687  dedekindicc  14812  coseq0q4123  15010  coseq0negpitopi  15012  relogeftb  15041  relogbcxpbap  15138  pwf1oexmid  15560  isomninnlem  15590  apdiff  15608  iswomninnlem  15609  ismkvnnlem  15612  redcwlpolemeq1  15614