Theorem impbida 801

Description: Deduce an equivalence from two implications. Variant of impbid 212. (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 212	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  biadanid  823  eqrdav  2734  eqsndOLD  4836  frsn  5776  funfvbrb  7071  iinpreima  7089  fcdmssb  7142  fnprb  7228  fntpb  7229  fpr2g  7231  nvocnv  7301  fsnex  7303  f1ocnv2d  7686  el2xptp0  8060  1stconst  8124  2ndconst  8125  cnvf1o  8135  fimaproj  8159  tfrlem15  8431  oeeui  8639  ersymb  8758  swoer  8775  erth  8795  boxriin  8979  boxcutc  8980  domunsncan  9111  pw2f1olem  9115  enen1  9156  enen2  9157  domen1  9158  domen2  9159  sdomen1  9160  sdomen2  9161  xpmapenlem  9183  ensymfib  9222  ordiso2  9553  wdomen1  9614  wdomen2  9615  fin23lem26  10363  fpwwe2lem7  10675  r1wunlim  10775  mul2lt0bi  13139  ixxun  13400  xov1plusxeqvd  13535  fzsplit2  13586  fseq1p1m1  13635  elfz2nn0  13655  flflp1  13844  modsubdir  13978  zesq  14262  expnngt1b  14278  hashprg  14431  hashgt0elexb  14438  hashbclem  14488  hashge2el2difb  14518  rereb  15156  rlimclim  15579  iserex  15690  caucvgb  15713  mptfzshft  15811  fsumrev  15812  climcnds  15884  fprodrev  16010  dvdsadd2b  16340  nn0ob  16418  bitsfzo  16469  dfgcd2  16580  dvdsmulgcd  16590  lcmgcdeq  16646  qden1elz  16791  mrcidb  17660  mrieqvlemd  17674  isacs2  17698  cicer  17854  ssclem  17867  issubc3  17900  ffthiso  17983  fuciso  18032  setcmon  18141  setcepi  18142  setcinv  18144  catciso  18165  acsfiindd  18611  issstrmgm  18679  mgmhmf1o  18726  issubmgm2  18729  subsubmgm  18736  resmgmhm2b  18739  issubmnd  18787  mhmf1o  18822  subsubm  18842  resmhm2b  18848  grpinvid1  19022  grpinvid2  19023  subsubg  19180  ssnmz  19197  ghmf1  19277  kerf1ghm  19278  ghmf1o  19279  conjnmzb  19284  subggim  19297  gicsubgen  19310  ghmqusnsglem1  19311  ghmquskerlem1  19314  ghmqusker  19318  gass  19332  odf1  19595  gex1  19624  fislw  19658  sylow3lem2  19661  sylow3lem6  19665  lsmdisj2a  19720  lsmdisj2b  19721  efgred2  19786  dmdprdsplit  20082  2nsgsimpgd  20137  simpgnsgbid  20138  ablsimpgd  20151  0unit  20413  irrednegb  20448  rnghmf1o  20469  rhmf1o  20508  subsubrng  20580  subrgunit  20607  subsubrg  20615  rngcinv  20654  ringcinv  20688  isdrng2  20760  issubdrg  20798  islss3  20975  islss4  20978  ellspsn6  21010  lspsneq0b  21029  islmhm2  21055  lmhmf1o  21063  reslmhm2b  21071  lssvs0or  21130  lvecinv  21133  ellspsn4  21144  lspdisjb  21146  islbs2  21174  islbs3  21175  dflidl2rng  21246  rngringbd  21336  prmirredlem  21501  islindf3  21864  lindsmm  21866  lsslindf  21868  lsslinds  21869  issubassa  21905  sraassab  21906  issubassa2  21930  gsumbagdiag  21969  subrgasclcl  22109  ply1scleq  22325  matunit  22700  slesolinvbi  22703  en2top  23008  elcls  23097  neindisj2  23147  neiptopnei  23156  neiptopreu  23157  maxlp  23171  neitr  23204  iscncl  23293  cncnp  23304  isreg2  23401  dis2ndc  23484  1stccnp  23486  islly2  23508  dislly  23521  dissnlocfin  23553  kgencmp2  23570  pt1hmeo  23830  xkocnv  23838  t0kq  23842  uffixfr  23947  flimcf  24006  cnpflf2  24024  fclscf  24049  cnextf  24090  utopsnneiplem  24272  isucn2  24304  cfilucfil  24588  psmetutop  24596  restmetu  24599  tngngp2  24689  tngngp  24691  nmoleub  24768  metdseq0  24890  cnheibor  25001  pcophtb  25076  nmoleub2lem  25161  lmmbr  25306  iscfil3  25321  cmetss  25364  cldcss  25489  mbfeqalem2  25691  mbfposb  25702  itg2const2  25791  itgss3  25865  plyco0  26246  dgrlt  26321  ulm2  26443  coseq00topi  26559  coseq0negpitopi  26560  sineq0  26581  relogbcxpb  26845  atans2  26989  xrlimcnp  27026  dchrelbas2  27296  dchrn0  27309  2sqb  27491  nosupbnd2  27776  noinfbnd2  27791  slerec  27879  sltmul2  28212  istrkg2ld  28483  tgcgreqb  28504  tgbtwncomb  28512  trgcgrg  28538  legov  28608  legov2  28609  legov3  28621  hlbtwn  28634  tglineelsb2  28655  tglinecom  28658  colline  28672  mirinv  28689  mirbtwnb  28695  mirbtwnhl  28703  perpcom  28736  isperp2  28738  oppcom  28767  opphllem3  28772  lnopp2hpgb  28786  colopp  28792  colhp  28793  lmieu  28807  iscgra1  28833  dfcgra2  28853  edgnbusgreu  29399  nb3grprlem1  29412  lfgriswlk  29721  eleclclwwlknlem2  30090  clwwlknscsh  30091  clwwlknon1  30126  numclwwlk2lem1  30405  grpoinvid1  30557  grpoinvid2  30558  leopmul  32163  hst1h  32256  bibiad  32486  eqelbid  32503  diffib  32549  ifnebib  32570  iinabrex  32589  disjabrex  32602  disjabrexf  32603  erbr3b  32637  f1o3d  32644  funimass4f  32654  2ndimaxp  32663  fgreu  32689  fcnvgreu  32690  1stpreimas  32721  fcobij  32740  resf1o  32748  nn0xmulclb  32782  fzsplit3  32802  fzo0opth  32813  eliccioo  32898  mgcmntco  32969  dfmgc2lem  32970  dfmgc2  32971  pwrssmgc  32975  mgcf1o  32978  mndlrinvb  33013  mndlactfo  33015  mndractfo  33017  mndlactf1o  33018  mndractf1o  33019  gsumhashmul  33047  gsumwrd2dccatlem  33052  ogrpinv0le  33075  ogrpaddltbi  33078  ogrpaddltrbid  33080  ogrpinv0lt  33082  cyc3genpm  33155  isarchi3  33177  prmsimpcyc  33217  domnlcanbOLD  33265  isdrng4  33279  fracerl  33288  qsxpid  33370  dvdsruasso  33393  dvdsruasso2  33394  dvdsrspss  33395  grplsmid  33412  quslsm  33413  nsgmgc  33420  nsgqusf1olem2  33422  nsgqusf1olem3  33423  pidlnzb  33430  unitpidl1  33432  elrspunidl  33436  elrspunsn  33437  drngidl  33441  drngidlhash  33442  isprmidlc  33455  prmidl0  33458  qsidom  33462  mxidlirred  33480  mxidlnzrb  33488  qsdrng  33505  rsprprmprmidlb  33531  rprmirredb  33540  deg1le0eq0  33578  ply1unit  33580  lvecdim0  33634  extdg1b  33692  irngnzply1  33706  1smat1  33765  ist0cld  33794  qtophaus  33797  reff  33800  locfinreflem  33801  cmpcref  33811  zarcls1  33830  zarclsun  33831  zarclsiin  33832  zarclssn  33834  metider  33855  pstmfval  33857  qqhval2  33945  aean  34225  imambfm  34244  eulerpartlemgvv  34358  orvcgteel  34449  orvclteel  34454  ballotlemsf1o  34495  sgn3da  34523  sgnnbi  34527  sgnpbi  34528  sgnmulsgn  34531  sgnmulsgp  34532  actfunsnf1o  34598  reprsuc  34609  reprpmtf1o  34620  sconnpi1  35224  brofs2  36059  brifs2  36060  broutsideof2  36104  bj-abv  36889  irrdiff  37309  ltflcei  37595  poimirlem25  37632  ismblfin  37648  cnambfre  37655  ftc1anclem6  37685  ismndo1  37860  isdrngo2  37945  eqvrelsymb  38588  eqvrelth  38593  lshpnelb  38966  lshpnel2N  38967  lsatspn0  38982  lsatelbN  38988  lsat0cv  39015  lcvexch  39021  lcv1  39023  lkrshp3  39088  lkrpssN  39145  lkrss2N  39151  cvlsupr2  39325  atcvrlln  39503  llncvrlpln  39541  2llnmj  39543  lplncvrlvol  39599  2lplnmj  39605  polcon2bN  39903  pcl0bN  39906  lhpmcvr3  40008  lhpmatb  40014  ltrncoidN  40111  ltrneq3  40191  ltrniotavalbN  40567  cdlemg1cN  40570  diclspsn  41177  dihopelvalcpre  41231  dihord4  41241  dihord  41247  dihmeetlem4preN  41289  dih1dimatlem0  41311  dochsscl  41351  dochoccl  41352  dochord  41353  dochsat  41366  dochshpncl  41367  dochsatshpb  41435  dochshpsat  41437  mapdval4N  41615  mapdsn  41624  hdmap14lem12  41862  hdmapip0  41898  hlhillcs  41945  riccrng  42509  ricdrng  42516  prjspner1  42613  mrefg2  42695  mzpmfp  42735  lzenom  42758  elpell14qr2  42850  elpell1qr2  42860  pellfund14b  42887  congabseq  42963  acongeq  42972  jm2.23  42985  jm2.20nn  42986  jm2.25lem1  42987  wepwsolem  43031  islssfg2  43060  lnmlmic  43077  dfacbasgrp  43097  unielss  43207  rfovcnvf1od  43994  dssmapnvod  44010  ntrclscls00  44056  rfcnpre3  44971  rfcnpre4  44972  ssmapsn  45159  rnmptssbi  45206  infxrgelbrnmpt  45404  xnegre  45416  xrpnf  45436  rexanuz2nf  45443  ioossioobi  45470  iccshift  45471  iocopn  45473  eliccelioc  45474  iooshift  45475  icoopn  45478  qinioo  45488  limcdm0  45574  islptre  45575  islpcn  45595  limcresioolb  45599  climuzlem  45699  climlimsup  45716  liminfgelimsup  45738  liminfgelimsupuz  45744  climliminf  45762  climliminflimsup  45764  climliminflimsup2  45765  xlimpnfxnegmnf  45770  xlimbr  45783  xlimmnfv  45790  xlimpnfv  45794  xlimclim2  45796  dfxlim2v  45803  climresdm  45806  xlimresdm  45815  xlimliminflimsup  45818  fperdvper  45875  itgperiod  45937  fourierdlem32  46095  fourierdlem33  46096  fourierdlem48  46110  fourierdlem49  46111  fourierdlem71  46133  fourierdlem81  46143  preimagelt  46655  preimalegt  46656  smfliminflem  46786  smfliminfmpt  46788  fcoresfob  47022  m1mod0mod1  47294  uspgrimprop  47811  isubgr3stgrlem8  47876  rngcinvALTV  48120  ringcinvALTV  48154  fvconstr  48686  fvconstrn0  48687  lubeldm2  48753  glbeldm2  48754  upeu2lem  48808  functhinclem1  48841  fullthinc  48846  thinciso  48861  prstchom2ALT  48880