Theorem impbida 873

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 449	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 449	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 201	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  eqrdav  2609  frsn  5112  elsnxpOLD  5595  funfvbrb  6238  iinpreima  6253  frnssb  6298  fnprb  6377  fntpb  6378  fpr2g  6380  nvocnv  6437  fsnex  6438  f1prex  6439  f1ocnv2d  6784  el2xptp0  7103  1stconst  7152  2ndconst  7153  cnvf1o  7163  tfrlem15  7375  oeeui  7569  ersymb  7643  swoer  7659  erth  7678  boxriin  7836  boxcutc  7837  domunsncan  7945  pw2f1olem  7949  enen1  7985  enen2  7986  domen1  7987  domen2  7988  sdomen1  7989  sdomen2  7990  xpmapenlem  8012  ordiso2  8303  wdomen1  8364  wdomen2  8365  fin23lem26  9030  fpwwe2lem8  9338  r1wunlim  9438  mul2lt0bi  11812  ixxun  12062  xov1plusxeqvd  12189  fzsplit2  12237  fseq1p1m1  12283  elfz2nn0  12300  flflp1  12470  modsubdir  12601  zesq  12849  hashprg  13043  hashprgOLD  13044  hashgt0elexb  13051  hashbclem  13093  hashge2el2difb  13119  rereb  13708  rlimclim  14125  iserex  14235  caucvgb  14258  mptfzshft  14352  fsumrev  14353  climcnds  14422  fprodrev  14546  dvdsadd2b  14866  nn0ob  14938  bitsfzo  14995  dfgcd2  15101  dvdsmulgcd  15112  lcmgcdeq  15163  qden1elz  15303  mrcidb  16098  mrieqvlemd  16112  isacs2  16137  cicer  16289  ssclem  16302  issubc3  16332  ffthiso  16412  fuciso  16458  setcmon  16560  setcepi  16561  setcinv  16563  catciso  16580  acsfiindd  17000  issstrmgm  17075  issubmnd  17141  mhmf1o  17168  subsubm  17180  resmhm2b  17184  grpinvid1  17293  grpinvid2  17294  subsubg  17440  ssnmz  17459  ghmf1  17512  ghmf1o  17513  conjnmzb  17518  subggim  17531  gicsubgen  17544  gass  17557  odf1  17802  gex1  17829  fislw  17863  sylow3lem2  17866  sylow3lem6  17870  lsmdisj2a  17923  lsmdisj2b  17924  efgred2  17989  dmdprdsplit  18269  0unit  18503  irrednegb  18534  rhmf1o  18555  kerf1hrm  18566  isdrng2  18580  subrgunit  18621  issubdrg  18628  subsubrg  18629  islss3  18780  islss4  18783  lspsnel6  18815  lspsneq0b  18834  islmhm2  18859  lmhmf1o  18867  reslmhm2b  18875  lssvs0or  18931  lvecinv  18934  lspsnel4  18945  lspdisjb  18947  islbs2  18975  islbs3  18976  issubassa  19145  issubassa2  19166  gsumbagdiag  19197  subrgasclcl  19320  prmirredlem  19660  islindf3  19984  lindsmm  19986  lsslindf  19988  lsslinds  19989  matunit  20303  slesolinvbi  20306  en2top  20600  elcls  20687  neindisj2  20737  neiptopnei  20746  neiptopreu  20747  maxlp  20761  neitr  20794  iscncl  20883  cncnp  20894  isreg2  20991  dis2ndc  21073  1stccnp  21075  islly2  21097  dislly  21110  dissnlocfin  21142  kgencmp2  21159  pt1hmeo  21419  xkocnv  21427  t0kq  21431  uffixfr  21537  flimcf  21596  cnpflf2  21614  fclscf  21639  cnextf  21680  utopsnneiplem  21861  isucn2  21893  cfilucfil  22174  psmetutop  22182  restmetu  22185  tngngp2  22266  tngngp  22268  nmoleub  22345  metdseq0  22465  cnheibor  22562  pcophtb  22637  nmoleub2lem  22722  lmmbr  22864  iscfil3  22879  cmetss  22921  cldcss  23020  mbfeqalem  23215  mbfposb  23226  itg2const2  23314  itgss3  23387  plyco0  23752  dgrlt  23826  ulm2  23943  coseq00topi  24058  coseq0negpitopi  24059  sineq0  24077  relogbcxpb  24325  atans2  24458  xrlimcnp  24495  dchrelbas2  24762  dchrn0  24775  2sqb  24957  istrkg2ld  25159  tgcgreqb  25176  tgbtwncomb  25184  trgcgrg  25210  legov  25280  legov2  25281  legov3  25293  hlbtwn  25306  tglineelsb2  25327  tglinecom  25330  colline  25344  mirinv  25361  mirbtwnb  25367  mirbtwnhl  25375  perpcom  25408  isperp2  25410  oppcom  25436  opphllem3  25441  lnopp2hpgb  25455  colopp  25461  colhp  25462  lmieu  25476  iscgra1  25502  dfcgra2  25521  nb3graprlem1  25980  eleclclwwlknlem2  26346  clwwlknscsh  26347  el2spthonot0  26398  numclwwlk2lem1  26629  grpoinvid1  26766  grpoinvid2  26767  leopmul  28377  hst1h  28470  disjabrex  28777  disjabrexf  28778  erbr3b  28807  f1o3d  28813  funimass4f  28818  fgreu  28854  fcnvgreu  28855  1stpreimas  28866  fcobij  28888  resf1o  28893  fzsplit3  28940  eliccioo  28970  ogrpinv0le  29047  ogrpaddltbi  29050  ogrpaddltrbid  29052  ogrpinv0lt  29054  isarchi3  29072  1smat1  29198  fimaproj  29228  qtophaus  29231  reff  29234  locfinreflem  29235  cmpcref  29245  metider  29265  pstmfval  29267  qqhval2  29354  aean  29634  imambfm  29651  eulerpartlemgvv  29765  orvcgteel  29856  orvclteel  29861  ballotlemsf1o  29902  sgn3da  29930  sgnnbi  29934  sgnpbi  29935  sgnmulsgn  29938  sgnmulsgp  29939  sconpi1  30475  brofs2  31354  brifs2  31355  broutsideof2  31399  ltflcei  32567  poimirlem25  32604  ismblfin  32620  cnambfre  32628  ftc1anclem6  32660  ismndo1  32842  isdrngo2  32927  lshpnelb  33289  lshpnel2N  33290  lsatspn0  33305  lsatelbN  33311  lsat0cv  33338  lcvexch  33344  lcv1  33346  lkrshp3  33411  lkrpssN  33468  lkrss2N  33474  cvlsupr2  33648  atcvrlln  33824  llncvrlpln  33862  2llnmj  33864  lplncvrlvol  33920  2lplnmj  33926  polcon2bN  34224  pcl0bN  34227  lhpmcvr3  34329  lhpmatb  34335  ltrncoidN  34432  ltrneq3  34513  ltrniotavalbN  34890  cdlemg1cN  34893  diclspsn  35501  dihopelvalcpre  35555  dihord4  35565  dihord  35571  dihmeetlem4preN  35613  dih1dimatlem0  35635  dochsscl  35675  dochoccl  35676  dochord  35677  dochsat  35690  dochshpncl  35691  dochsatshpb  35759  dochshpsat  35761  mapdval4N  35939  mapdsn  35948  hdmap14lem12  36189  hdmapip0  36225  hlhillcs  36268  mrefg2  36288  mzpmfp  36328  lzenom  36351  elpell14qr2  36444  elpell1qr2  36454  pellfund14b  36481  congabseq  36559  acongeq  36568  jm2.23  36581  jm2.20nn  36582  jm2.25lem1  36583  wepwsolem  36630  islssfg2  36659  lnmlmic  36676  dfacbasgrp  36697  rfovcnvf1od  37318  dssmapnvod  37334  ntrclscls00  37384  rfcnpre3  38215  rfcnpre4  38216  ioossioobi  38590  iccshift  38591  iocopn  38593  eliccelioc  38594  iooshift  38595  icoopn  38598  qinioo  38609  limcdm0  38685  islptre  38686  islpcn  38706  limcresioolb  38710  fperdvper  38808  itgperiod  38873  fourierdlem32  39032  fourierdlem33  39033  fourierdlem48  39047  fourierdlem49  39048  fourierdlem71  39070  fourierdlem81  39080  m1mod0mod1  39949  edgnbusgreu  40595  nb3grprlem1  40608  lfgriswlk  40897  eleclclwwlksnlem2  41246  clwwlksnscsh  41247  av-numclwwlk2lem1  41532  mgmhmf1o  41577  issubmgm2  41580  subsubmgm  41587  resmgmhm2b  41590  rnghmf1o  41693  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848