Theorem impbida 797

Description: Deduce an equivalence from two implications. Variant of impbid 211. (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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 412	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 211	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  biadanid  819  eqrdav  2737  frsn  5665  funfvbrb  6910  iinpreima  6928  frnssb  6977  fnprb  7066  fntpb  7067  fpr2g  7069  nvocnv  7134  fsnex  7135  f1ocnv2d  7500  el2xptp0  7851  1stconst  7911  2ndconst  7912  cnvf1o  7922  fimaproj  7947  tfrlem15  8194  oeeui  8395  ersymb  8470  swoer  8486  erth  8505  boxriin  8686  boxcutc  8687  domunsncan  8812  pw2f1olem  8816  enen1  8853  enen2  8854  domen1  8855  domen2  8856  sdomen1  8857  sdomen2  8858  xpmapenlem  8880  ensymfib  8930  ordiso2  9204  wdomen1  9265  wdomen2  9266  fin23lem26  10012  fpwwe2lem7  10324  r1wunlim  10424  mul2lt0bi  12765  ixxun  13024  xov1plusxeqvd  13159  fzsplit2  13210  fseq1p1m1  13259  elfz2nn0  13276  flflp1  13455  modsubdir  13588  zesq  13869  expnngt1b  13885  hashprg  14038  hashgt0elexb  14045  hashbclem  14092  hashge2el2difb  14124  rereb  14759  rlimclim  15183  iserex  15296  caucvgb  15319  mptfzshft  15418  fsumrev  15419  climcnds  15491  fprodrev  15615  dvdsadd2b  15943  nn0ob  16021  bitsfzo  16070  dfgcd2  16182  dvdsmulgcd  16193  lcmgcdeq  16245  qden1elz  16389  mrcidb  17241  mrieqvlemd  17255  isacs2  17279  cicer  17435  ssclem  17448  issubc3  17480  ffthiso  17561  fuciso  17609  setcmon  17718  setcepi  17719  setcinv  17721  catciso  17742  acsfiindd  18186  issstrmgm  18252  issubmnd  18327  mhmf1o  18355  subsubm  18370  resmhm2b  18376  grpinvid1  18545  grpinvid2  18546  subsubg  18693  ssnmz  18709  ghmf1  18778  ghmf1o  18779  conjnmzb  18784  subggim  18797  gicsubgen  18809  gass  18822  odf1  19084  gex1  19111  fislw  19145  sylow3lem2  19148  sylow3lem6  19152  lsmdisj2a  19208  lsmdisj2b  19209  efgred2  19274  dmdprdsplit  19565  2nsgsimpgd  19620  simpgnsgbid  19621  ablsimpgd  19634  0unit  19837  irrednegb  19868  rhmf1o  19891  kerf1ghm  19902  isdrng2  19916  subrgunit  19957  issubdrg  19964  subsubrg  19965  islss3  20136  islss4  20139  lspsnel6  20171  lspsneq0b  20190  islmhm2  20215  lmhmf1o  20223  reslmhm2b  20231  lssvs0or  20287  lvecinv  20290  lspsnel4  20301  lspdisjb  20303  islbs2  20331  islbs3  20332  prmirredlem  20606  islindf3  20943  lindsmm  20945  lsslindf  20947  lsslinds  20948  issubassa  20983  issubassa2  21006  gsumbagdiagOLD  21052  gsumbagdiag  21055  subrgasclcl  21185  matunit  21735  slesolinvbi  21738  en2top  22043  elcls  22132  neindisj2  22182  neiptopnei  22191  neiptopreu  22192  maxlp  22206  neitr  22239  iscncl  22328  cncnp  22339  isreg2  22436  dis2ndc  22519  1stccnp  22521  islly2  22543  dislly  22556  dissnlocfin  22588  kgencmp2  22605  pt1hmeo  22865  xkocnv  22873  t0kq  22877  uffixfr  22982  flimcf  23041  cnpflf2  23059  fclscf  23084  cnextf  23125  utopsnneiplem  23307  isucn2  23339  cfilucfil  23621  psmetutop  23629  restmetu  23632  tngngp2  23722  tngngp  23724  nmoleub  23801  metdseq0  23923  cnheibor  24024  pcophtb  24098  nmoleub2lem  24183  lmmbr  24327  iscfil3  24342  cmetss  24385  cldcss  24510  mbfeqalem2  24711  mbfposb  24722  itg2const2  24811  itgss3  24884  plyco0  25258  dgrlt  25332  ulm2  25449  coseq00topi  25564  coseq0negpitopi  25565  sineq0  25585  relogbcxpb  25842  atans2  25986  xrlimcnp  26023  dchrelbas2  26290  dchrn0  26303  2sqb  26485  istrkg2ld  26725  tgcgreqb  26746  tgbtwncomb  26754  trgcgrg  26780  legov  26850  legov2  26851  legov3  26863  hlbtwn  26876  tglineelsb2  26897  tglinecom  26900  colline  26914  mirinv  26931  mirbtwnb  26937  mirbtwnhl  26945  perpcom  26978  isperp2  26980  oppcom  27009  opphllem3  27014  lnopp2hpgb  27028  colopp  27034  colhp  27035  lmieu  27049  iscgra1  27075  dfcgra2  27095  edgnbusgreu  27637  nb3grprlem1  27650  lfgriswlk  27958  eleclclwwlknlem2  28326  clwwlknscsh  28327  clwwlknon1  28362  numclwwlk2lem1  28641  grpoinvid1  28791  grpoinvid2  28792  leopmul  30397  hst1h  30490  diffib  30770  eqsnd  30778  iinabrex  30809  disjabrex  30822  disjabrexf  30823  erbr3b  30858  f1o3d  30863  funimass4f  30873  2ndimaxp  30885  fgreu  30911  fcnvgreu  30912  1stpreimas  30940  fcobij  30959  resf1o  30967  nn0xmulclb  30996  fzsplit3  31017  eliccioo  31107  mgcmntco  31174  dfmgc2lem  31175  dfmgc2  31176  pwrssmgc  31180  mgcf1o  31183  gsumhashmul  31218  ogrpinv0le  31243  ogrpaddltbi  31246  ogrpaddltrbid  31248  ogrpinv0lt  31250  cyc3genpm  31321  isarchi3  31343  prmsimpcyc  31383  qsxpid  31460  grplsmid  31494  quslsm  31495  nsgmgc  31499  nsgqusf1olem2  31501  nsgqusf1olem3  31502  elrspunidl  31508  isprmidlc  31525  prmidl0  31528  qsidom  31532  mxidlnzrb  31546  ply1scleq  31570  lvecdim0  31592  extdg1b  31641  1smat1  31656  ist0cld  31685  qtophaus  31688  reff  31691  locfinreflem  31692  cmpcref  31702  zarcls1  31721  zarclsun  31722  zarclsiin  31723  zarclssn  31725  metider  31746  pstmfval  31748  qqhval2  31832  aean  32112  imambfm  32129  eulerpartlemgvv  32243  orvcgteel  32334  orvclteel  32339  ballotlemsf1o  32380  sgn3da  32408  sgnnbi  32412  sgnpbi  32413  sgnmulsgn  32416  sgnmulsgp  32417  actfunsnf1o  32484  reprsuc  32495  reprpmtf1o  32506  sconnpi1  33101  nosupbnd2  33846  noinfbnd2  33861  slerec  33940  brofs2  34306  brifs2  34307  broutsideof2  34351  bj-abv  35018  irrdiff  35424  ltflcei  35692  poimirlem25  35729  ismblfin  35745  cnambfre  35752  ftc1anclem6  35782  ismndo1  35958  isdrngo2  36043  eqvrelsymb  36646  eqvrelth  36651  lshpnelb  36925  lshpnel2N  36926  lsatspn0  36941  lsatelbN  36947  lsat0cv  36974  lcvexch  36980  lcv1  36982  lkrshp3  37047  lkrpssN  37104  lkrss2N  37110  cvlsupr2  37284  atcvrlln  37461  llncvrlpln  37499  2llnmj  37501  lplncvrlvol  37557  2lplnmj  37563  polcon2bN  37861  pcl0bN  37864  lhpmcvr3  37966  lhpmatb  37972  ltrncoidN  38069  ltrneq3  38149  ltrniotavalbN  38525  cdlemg1cN  38528  diclspsn  39135  dihopelvalcpre  39189  dihord4  39199  dihord  39205  dihmeetlem4preN  39247  dih1dimatlem0  39269  dochsscl  39309  dochoccl  39310  dochord  39311  dochsat  39324  dochshpncl  39325  dochsatshpb  39393  dochshpsat  39395  mapdval4N  39573  mapdsn  39582  hdmap14lem12  39820  hdmapip0  39856  hlhillcs  39903  prjspner1  40384  mrefg2  40445  mzpmfp  40485  lzenom  40508  elpell14qr2  40600  elpell1qr2  40610  pellfund14b  40637  congabseq  40712  acongeq  40721  jm2.23  40734  jm2.20nn  40735  jm2.25lem1  40736  wepwsolem  40783  islssfg2  40812  lnmlmic  40829  dfacbasgrp  40849  rfovcnvf1od  41501  dssmapnvod  41517  ntrclscls00  41565  rfcnpre3  42465  rfcnpre4  42466  rnmptssbi  42696  infxrgelbrnmpt  42884  xnegre  42896  xrpnf  42916  ioossioobi  42945  iccshift  42946  iocopn  42948  eliccelioc  42949  iooshift  42950  icoopn  42953  qinioo  42963  limcdm0  43049  islptre  43050  islpcn  43070  limcresioolb  43074  climuzlem  43174  climlimsup  43191  liminfgelimsup  43213  liminfgelimsupuz  43219  climliminf  43237  climliminflimsup  43239  climliminflimsup2  43240  xlimpnfxnegmnf  43245  xlimbr  43258  xlimmnfv  43265  xlimpnfv  43269  xlimclim2  43271  dfxlim2v  43278  climresdm  43281  xlimresdm  43290  xlimliminflimsup  43293  fperdvper  43350  itgperiod  43412  fourierdlem32  43570  fourierdlem33  43571  fourierdlem48  43585  fourierdlem49  43586  fourierdlem71  43608  fourierdlem81  43618  preimagelt  44126  preimalegt  44127  smfliminflem  44250  smfliminfmpt  44252  fcoresfob  44453  m1mod0mod1  44709  mgmhmf1o  45229  issubmgm2  45232  subsubmgm  45239  resmgmhm2b  45242  rnghmf1o  45349  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  fvconstr  46071  fvconstrn0  46072  lubeldm2  46138  glbeldm2  46139  functhinclem1  46210  fullthinc  46215  thinciso  46229  prstchom2ALT  46246