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  7319  2omapfi  7321  ordiso2  7376  omniwomnimkv  7508  enwomnilem  7510  nninfwlpoimlemginf  7517  pw1if  7585  exmidapne  7627  infregelbex  10008  fzsplit2  10466  fzsplit3  10469  fseq1p1m1  10512  elfz2nn0  10530  infssfzcldc  10680  infssfzledc  10681  btwnzge0  10750  modqsubdir  10845  zesq  11111  hashprg  11265  sseqn  11295  hashfibclem  11298  rereb  11644  abslt  11871  absle  11872  maxleastb  11997  maxltsup  12001  xrltmaxsup  12042  xrmaxltsup  12043  iserex  12124  mptfzshft  12228  fsumrev  12229  fprodrev  12405  dvdsadd2b  12626  nn0ob  12694  bitsfzo  12741  dfgcd3  12806  dfgcd2  12810  dvdsmulgcd  12821  lcmgcdeq  12880  isprm5  12940  nnmaxpwlemparts  12971  qden1elz  13004  ballotfilemsf1o  13309  issubmnd  13808  mhmf1o  13830  subsubm  13843  resmhm2b  13849  grpinvid1  13910  grpinvid2  13911  subsubg  14053  ssnmz  14067  ghmf1  14129  kerf1ghm  14130  ghmf1o  14131  conjnmzb  14136  0unit  14520  rhmf1o  14559  subsubrng  14606  subrgunit  14631  subsubrg  14637  ringunitap  14677  drngunitap  14692  islss3  14800  islss4  14803  ellspsn6  14829  lspsneq0b  14848  dflidl2rng  14902  issubassa  15097  issubassa2  15119  psrbaglefifi  15147  cncnp  15422  xmetxpbl  15700  dedekindicc  15825  coseq0q4123  16027  coseq0negpitopi  16029  relogeftb  16058  relogbcxpbap  16162  upgr2wlkdc  16784  pw1map  17191  pwf1oexmid  17195  isomninnlem  17245  apdiff  17264  iswomninnlem  17266  ismkvnnlem  17269  redcwlpolemeq1  17271