Theorem impbida 799

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

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

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 397

This theorem is referenced by:  biadanid  821  eqrdav  2730  frsn  5755  funfvbrb  7037  iinpreima  7055  fcdmssb  7105  fnprb  7194  fntpb  7195  fpr2g  7197  nvocnv  7263  fsnex  7265  f1ocnv2d  7642  el2xptp0  8004  1stconst  8068  2ndconst  8069  cnvf1o  8079  fimaproj  8103  tfrlem15  8374  oeeui  8585  ersymb  8700  swoer  8716  erth  8735  boxriin  8917  boxcutc  8918  domunsncan  9055  pw2f1olem  9059  enen1  9100  enen2  9101  domen1  9102  domen2  9103  sdomen1  9104  sdomen2  9105  xpmapenlem  9127  ensymfib  9170  ordiso2  9492  wdomen1  9553  wdomen2  9554  fin23lem26  10302  fpwwe2lem7  10614  r1wunlim  10714  mul2lt0bi  13062  ixxun  13322  xov1plusxeqvd  13457  fzsplit2  13508  fseq1p1m1  13557  elfz2nn0  13574  flflp1  13754  modsubdir  13887  zesq  14171  expnngt1b  14187  hashprg  14337  hashgt0elexb  14344  hashbclem  14393  hashge2el2difb  14425  rereb  15049  rlimclim  15472  iserex  15585  caucvgb  15608  mptfzshft  15706  fsumrev  15707  climcnds  15779  fprodrev  15903  dvdsadd2b  16231  nn0ob  16309  bitsfzo  16358  dfgcd2  16470  dvdsmulgcd  16479  lcmgcdeq  16531  qden1elz  16675  mrcidb  17541  mrieqvlemd  17555  isacs2  17579  cicer  17735  ssclem  17748  issubc3  17781  ffthiso  17862  fuciso  17910  setcmon  18019  setcepi  18020  setcinv  18022  catciso  18043  acsfiindd  18488  issstrmgm  18554  issubmnd  18629  mhmf1o  18658  subsubm  18673  resmhm2b  18679  grpinvid1  18851  grpinvid2  18852  subsubg  19001  ssnmz  19018  ghmf1  19087  ghmf1o  19088  conjnmzb  19093  subggim  19106  gicsubgen  19118  gass  19131  odf1  19394  gex1  19423  fislw  19457  sylow3lem2  19460  sylow3lem6  19464  lsmdisj2a  19519  lsmdisj2b  19520  efgred2  19585  dmdprdsplit  19876  2nsgsimpgd  19931  simpgnsgbid  19932  ablsimpgd  19945  0unit  20162  irrednegb  20195  rhmf1o  20219  kerf1ghm  20232  isdrng2  20278  subrgunit  20330  issubdrg  20338  subsubrg  20339  islss3  20519  islss4  20522  lspsnel6  20554  lspsneq0b  20573  islmhm2  20598  lmhmf1o  20606  reslmhm2b  20614  lssvs0or  20672  lvecinv  20675  lspsnel4  20686  lspdisjb  20688  islbs2  20716  islbs3  20717  prmirredlem  20975  islindf3  21314  lindsmm  21316  lsslindf  21318  lsslinds  21319  issubassa  21354  issubassa2  21377  gsumbagdiagOLD  21423  gsumbagdiag  21426  subrgasclcl  21557  matunit  22109  slesolinvbi  22112  en2top  22417  elcls  22506  neindisj2  22556  neiptopnei  22565  neiptopreu  22566  maxlp  22580  neitr  22613  iscncl  22702  cncnp  22713  isreg2  22810  dis2ndc  22893  1stccnp  22895  islly2  22917  dislly  22930  dissnlocfin  22962  kgencmp2  22979  pt1hmeo  23239  xkocnv  23247  t0kq  23251  uffixfr  23356  flimcf  23415  cnpflf2  23433  fclscf  23458  cnextf  23499  utopsnneiplem  23681  isucn2  23713  cfilucfil  23997  psmetutop  24005  restmetu  24008  tngngp2  24098  tngngp  24100  nmoleub  24177  metdseq0  24299  cnheibor  24400  pcophtb  24474  nmoleub2lem  24559  lmmbr  24704  iscfil3  24719  cmetss  24762  cldcss  24887  mbfeqalem2  25088  mbfposb  25099  itg2const2  25188  itgss3  25261  plyco0  25635  dgrlt  25709  ulm2  25826  coseq00topi  25941  coseq0negpitopi  25942  sineq0  25962  relogbcxpb  26219  atans2  26363  xrlimcnp  26400  dchrelbas2  26667  dchrn0  26680  2sqb  26862  nosupbnd2  27146  noinfbnd2  27161  slerec  27246  sltmul2  27534  istrkg2ld  27576  tgcgreqb  27597  tgbtwncomb  27605  trgcgrg  27631  legov  27701  legov2  27702  legov3  27714  hlbtwn  27727  tglineelsb2  27748  tglinecom  27751  colline  27765  mirinv  27782  mirbtwnb  27788  mirbtwnhl  27796  perpcom  27829  isperp2  27831  oppcom  27860  opphllem3  27865  lnopp2hpgb  27879  colopp  27885  colhp  27886  lmieu  27900  iscgra1  27926  dfcgra2  27946  edgnbusgreu  28489  nb3grprlem1  28502  lfgriswlk  28810  eleclclwwlknlem2  29179  clwwlknscsh  29180  clwwlknon1  29215  numclwwlk2lem1  29494  grpoinvid1  29644  grpoinvid2  29645  leopmul  31250  hst1h  31343  eqelbid  31578  diffib  31623  eqsnd  31631  ifnebib  31646  iinabrex  31665  disjabrex  31678  disjabrexf  31679  erbr3b  31714  f1o3d  31719  funimass4f  31729  2ndimaxp  31741  fgreu  31766  fcnvgreu  31767  1stpreimas  31798  fcobij  31818  resf1o  31826  nn0xmulclb  31855  fzsplit3  31876  eliccioo  31968  mgcmntco  32035  dfmgc2lem  32036  dfmgc2  32037  pwrssmgc  32041  mgcf1o  32044  gsumhashmul  32079  ogrpinv0le  32104  ogrpaddltbi  32107  ogrpaddltrbid  32109  ogrpinv0lt  32111  cyc3genpm  32182  isarchi3  32204  prmsimpcyc  32244  isdrng4  32257  qsxpid  32336  grplsmid  32372  quslsm  32374  nsgmgc  32379  nsgqusf1olem2  32381  nsgqusf1olem3  32382  ghmquskerlem1  32384  ghmqusker  32387  elrspunidl  32397  elrspunsn  32398  drngidl  32402  drngidlhash  32403  isprmidlc  32417  prmidl0  32420  qsidom  32424  mxidlnzrb  32441  qsdrng  32457  ply1scleq  32484  lvecdim0  32530  extdg1b  32581  irngnzply1  32593  1smat1  32615  ist0cld  32644  qtophaus  32647  reff  32650  locfinreflem  32651  cmpcref  32661  zarcls1  32680  zarclsun  32681  zarclsiin  32682  zarclssn  32684  metider  32705  pstmfval  32707  qqhval2  32793  aean  33073  imambfm  33092  eulerpartlemgvv  33206  orvcgteel  33297  orvclteel  33302  ballotlemsf1o  33343  sgn3da  33371  sgnnbi  33375  sgnpbi  33376  sgnmulsgn  33379  sgnmulsgp  33380  actfunsnf1o  33447  reprsuc  33458  reprpmtf1o  33469  sconnpi1  34061  brofs2  34879  brifs2  34880  broutsideof2  34924  bj-abv  35590  irrdiff  36011  ltflcei  36280  poimirlem25  36317  ismblfin  36333  cnambfre  36340  ftc1anclem6  36370  ismndo1  36546  isdrngo2  36631  eqvrelsymb  37281  eqvrelth  37286  lshpnelb  37659  lshpnel2N  37660  lsatspn0  37675  lsatelbN  37681  lsat0cv  37708  lcvexch  37714  lcv1  37716  lkrshp3  37781  lkrpssN  37838  lkrss2N  37844  cvlsupr2  38018  atcvrlln  38196  llncvrlpln  38234  2llnmj  38236  lplncvrlvol  38292  2lplnmj  38298  polcon2bN  38596  pcl0bN  38599  lhpmcvr3  38701  lhpmatb  38707  ltrncoidN  38804  ltrneq3  38884  ltrniotavalbN  39260  cdlemg1cN  39263  diclspsn  39870  dihopelvalcpre  39924  dihord4  39934  dihord  39940  dihmeetlem4preN  39982  dih1dimatlem0  40004  dochsscl  40044  dochoccl  40045  dochord  40046  dochsat  40059  dochshpncl  40060  dochsatshpb  40128  dochshpsat  40130  mapdval4N  40308  mapdsn  40317  hdmap14lem12  40555  hdmapip0  40591  hlhillcs  40638  riccrng  40901  ricdrng  40907  prjspner1  41150  mrefg2  41216  mzpmfp  41256  lzenom  41279  elpell14qr2  41371  elpell1qr2  41381  pellfund14b  41408  congabseq  41484  acongeq  41493  jm2.23  41506  jm2.20nn  41507  jm2.25lem1  41508  wepwsolem  41555  islssfg2  41584  lnmlmic  41601  dfacbasgrp  41621  unielss  41738  rfovcnvf1od  42526  dssmapnvod  42542  ntrclscls00  42588  rfcnpre3  43488  rfcnpre4  43489  rnmptssbi  43738  infxrgelbrnmpt  43937  xnegre  43949  xrpnf  43969  rexanuz2nf  43976  ioossioobi  44003  iccshift  44004  iocopn  44006  eliccelioc  44007  iooshift  44008  icoopn  44011  qinioo  44021  limcdm0  44107  islptre  44108  islpcn  44128  limcresioolb  44132  climuzlem  44232  climlimsup  44249  liminfgelimsup  44271  liminfgelimsupuz  44277  climliminf  44295  climliminflimsup  44297  climliminflimsup2  44298  xlimpnfxnegmnf  44303  xlimbr  44316  xlimmnfv  44323  xlimpnfv  44327  xlimclim2  44329  dfxlim2v  44336  climresdm  44339  xlimresdm  44348  xlimliminflimsup  44351  fperdvper  44408  itgperiod  44470  fourierdlem32  44628  fourierdlem33  44629  fourierdlem48  44643  fourierdlem49  44644  fourierdlem71  44666  fourierdlem81  44676  preimagelt  45188  preimalegt  45189  smfliminflem  45319  smfliminfmpt  45321  fcoresfob  45554  m1mod0mod1  45809  mgmhmf1o  46329  issubmgm2  46332  subsubmgm  46339  resmgmhm2b  46342  rnghmf1o  46449  rngcinv  46527  rngcinvALTV  46539  ringcinv  46578  ringcinvALTV  46602  fvconstr  47170  fvconstrn0  47171  lubeldm2  47237  glbeldm2  47238  functhinclem1  47309  fullthinc  47314  thinciso  47328  prstchom2ALT  47347