Theorem impbida 604

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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadanid  622  eqrdav  2237  funfvbrb  5822  f1ocnv2d  6294  f1o3d  6298  funimass4f  6359  1stconst  6457  2ndconst  6458  cnvf1o  6461  ersymb  6821  swoer  6835  erth  6853  pw2f1odclem  7134  enen1  7140  enen2  7141  domen1  7142  domen2  7143  xpmapenlem  7149  fidifsnen  7172  fundmfibi  7252  f1dmvrnfibi  7258  2omap  7318  2omapfi  7320  ordiso2  7375  omniwomnimkv  7507  enwomnilem  7509  nninfwlpoimlemginf  7516  pw1if  7584  exmidapne  7626  infregelbex  10007  fzsplit2  10465  fzsplit3  10468  fseq1p1m1  10511  elfz2nn0  10529  infssfzcldc  10679  infssfzledc  10680  btwnzge0  10748  modqsubdir  10843  zesq  11109  hashprg  11263  sseqn  11293  hashfibclem  11296  rereb  11642  abslt  11869  absle  11870  maxleastb  11995  maxltsup  11999  xrltmaxsup  12039  xrmaxltsup  12040  iserex  12121  mptfzshft  12225  fsumrev  12226  fprodrev  12402  dvdsadd2b  12623  nn0ob  12691  bitsfzo  12738  dfgcd3  12803  dfgcd2  12807  dvdsmulgcd  12818  lcmgcdeq  12877  isprm5  12937  nnmaxpwlemparts  12968  qden1elz  13001  ballotfilemsf1o  13306  issubmnd  13804  mhmf1o  13826  subsubm  13839  resmhm2b  13845  grpinvid1  13906  grpinvid2  13907  subsubg  14049  ssnmz  14063  ghmf1  14125  kerf1ghm  14126  ghmf1o  14127  conjnmzb  14132  0unit  14485  rhmf1o  14524  subsubrng  14571  subrgunit  14596  subsubrg  14602  ringunitap  14642  drngunitap  14657  islss3  14765  islss4  14768  ellspsn6  14794  lspsneq0b  14813  dflidl2rng  14867  issubassa  15062  issubassa2  15084  cncnp  15380  xmetxpbl  15658  dedekindicc  15783  coseq0q4123  15985  coseq0negpitopi  15987  relogeftb  16016  relogbcxpbap  16120  upgr2wlkdc  16716  pw1map  17123  pwf1oexmid  17127  isomninnlem  17177  apdiff  17195  iswomninnlem  17197  ismkvnnlem  17200  redcwlpolemeq1  17202