Theorem impbida 806

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

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

This theorem is referenced by:  biadanid  828  bibiad  845  eqsndOLD  4762  frsn  5706  funfvbrb  6992  iinpreima  7010  fcdmssb  7063  fnprb  7152  fntpb  7153  fpr2g  7155  nvocnv  7225  fsnex  7227  f1ocnv2d  7609  resf1extb  7874  el2xptp0  7978  1stconst  8039  2ndconst  8040  cnvf1o  8050  fimaproj  8075  tfrlem15  8321  oeeui  8528  ersymb  8648  swoer  8665  erth  8688  boxriin  8878  boxcutc  8879  domunsncan  9005  pw2f1olem  9009  enen1  9045  enen2  9046  domen1  9047  domen2  9048  sdomen1  9049  sdomen2  9050  xpmapenlem  9072  ensymfib  9108  ordiso2  9420  wdomen1  9481  wdomen2  9482  fin23lem26  10238  fpwwe2lem7  10551  r1wunlim  10651  mul2lt0bi  13041  ixxun  13305  xov1plusxeqvd  13442  fzsplit2  13494  fseq1p1m1  13543  elfz2nn0  13563  flflp1  13757  modaddb  13859  modsubdir  13893  zesq  14179  expnngt1b  14195  hashprg  14348  hashgt0elexb  14355  hashbclem  14405  hashge2el2difb  14435  rereb  15073  rlimclim  15499  iserex  15610  caucvgb  15633  mptfzshft  15731  fsumrev  15732  climcnds  15807  fprodrev  15933  dvdsadd2b  16266  nn0ob  16344  bitsfzo  16395  dfgcd2  16506  dvdsmulgcd  16516  lcmgcdeq  16572  qden1elz  16718  mrcidb  17572  mrieqvlemd  17586  isacs2  17610  cicer  17764  ssclem  17777  issubc3  17807  ffthiso  17889  fuciso  17936  setcmon  18045  setcepi  18046  setcinv  18048  catciso  18069  acsfiindd  18510  issstrmgm  18612  mgmhmf1o  18659  issubmgm2  18662  subsubmgm  18669  resmgmhm2b  18672  issubmnd  18720  mhmf1o  18755  subsubm  18775  resmhm2b  18781  grpinvid1  18958  grpinvid2  18959  subsubg  19116  ssnmz  19132  ghmf1  19212  kerf1ghm  19213  ghmf1o  19214  conjnmzb  19219  subggim  19232  gicsubgen  19245  ghmqusnsglem1  19246  ghmquskerlem1  19249  ghmqusker  19253  gass  19267  odf1  19528  gex1  19557  fislw  19591  sylow3lem2  19594  sylow3lem6  19598  lsmdisj2a  19653  lsmdisj2b  19654  efgred2  19719  dmdprdsplit  20015  2nsgsimpgd  20070  simpgnsgbid  20071  ablsimpgd  20084  ogrpinv0le  20102  ogrpaddltbi  20105  ogrpaddltrbid  20107  ogrpinv0lt  20109  0unit  20367  irrednegb  20402  rnghmf1o  20423  rhmf1o  20462  subsubrng  20535  subrgunit  20562  subsubrg  20570  rngcinv  20609  ringcinv  20643  isdrng2  20715  issubdrg  20752  islss3  20949  islss4  20952  ellspsn6  20984  lspsneq0b  21003  islmhm2  21028  lmhmf1o  21036  reslmhm2b  21044  lssvs0or  21103  lvecinv  21106  ellspsn4  21117  lspdisjb  21119  islbs2  21147  islbs3  21148  dflidl2rng  21211  rngringbd  21301  prmirredlem  21447  islindf3  21801  lindsmm  21803  lsslindf  21805  lsslinds  21806  issubassa  21842  sraassab  21843  issubassa2  21867  gsumbagdiag  21907  subrgasclcl  22043  ply1scleq  22291  matunit  22661  slesolinvbi  22664  en2top  22968  elcls  23056  neindisj2  23106  neiptopnei  23115  neiptopreu  23116  maxlp  23130  neitr  23163  iscncl  23252  cncnp  23263  isreg2  23360  dis2ndc  23443  1stccnp  23445  islly2  23467  dislly  23480  dissnlocfin  23512  kgencmp2  23529  pt1hmeo  23789  xkocnv  23797  t0kq  23801  uffixfr  23906  flimcf  23965  cnpflf2  23983  fclscf  24008  cnextf  24049  utopsnneiplem  24230  isucn2  24261  cfilucfil  24542  psmetutop  24550  restmetu  24553  tngngp2  24635  tngngp  24637  nmoleub  24714  metdseq0  24838  cnheibor  24940  pcophtb  25014  nmoleub2lem  25099  lmmbr  25243  iscfil3  25258  cmetss  25301  cldcss  25426  mbfeqalem2  25627  mbfposb  25638  itg2const2  25726  itgss3  25800  plyco0  26175  dgrlt  26249  ulm2  26368  coseq00topi  26484  coseq0negpitopi  26485  sineq0  26506  relogbcxpb  26769  atans2  26913  xrlimcnp  26950  dchrelbas2  27218  dchrn0  27231  2sqb  27413  nosupbnd2  27698  noinfbnd2  27713  lesrec  27809  ltmuls2  28181  elreno2  28505  istrkg2ld  28546  tgcgreqb  28567  tgbtwncomb  28575  trgcgrg  28601  legov  28671  legov2  28672  legov3  28684  hlbtwn  28697  tglineelsb2  28718  tglinecom  28721  colline  28735  mirinv  28752  mirbtwnb  28758  mirbtwnhl  28766  perpcom  28799  isperp2  28801  oppcom  28830  opphllem3  28835  lnopp2hpgb  28849  colopp  28855  colhp  28856  lmieu  28870  iscgra1  28896  dfcgra2  28916  edgnbusgreu  29454  nb3grprlem1  29467  lfgriswlk  29773  eleclclwwlknlem2  30149  clwwlknscsh  30150  clwwlknon1  30185  numclwwlk2lem1  30464  grpoinvid1  30617  grpoinvid2  30618  leopmul  32223  hst1h  32316  eqelbid  32562  diffib  32609  ifnebib  32637  iinabrex  32658  disjabrex  32671  disjabrexf  32672  erbr3b  32709  f1o3d  32718  funimass4f  32729  2ndimaxp  32738  fgreu  32763  fcnvgreu  32764  1stpreimas  32798  fcobij  32812  cocnvf1o  32821  resf1o  32822  nn0xmulclb  32863  fzsplit3  32885  fzo0opth  32895  sgn3da  32926  sgnnbi  32930  sgnpbi  32931  sgnmulsgn  32934  sgnmulsgp  32935  eliccioo  33009  mgcmntco  33073  dfmgc2lem  33074  dfmgc2  33075  pwrssmgc  33079  mgcf1o  33082  mndlrinvb  33104  mndlactfo  33106  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  gsumhashmul  33148  gsumwrd2dccatlem  33158  cyc3genpm  33233  isarchi3  33268  prmsimpcyc  33309  elrgspnsubrunlem1  33328  elrgspnsubrun  33330  domnlcanbOLD  33362  ricdomn  33371  isdrng4  33379  fracerl  33390  qsxpid  33445  dvdsruasso  33468  dvdsruasso2  33469  dvdsrspss  33470  grplsmid  33487  quslsm  33488  nsgmgc  33495  nsgqusf1olem2  33497  nsgqusf1olem3  33498  pidlnzb  33505  unitpidl1  33507  elrspunidl  33511  elrspunsn  33512  drngidl  33516  drngidlhash  33517  isprmidlc  33530  prmidl0  33533  qsidom  33537  mxidlirred  33555  mxidlnzrb  33563  qsdrng  33580  rsprprmprmidlb  33606  rprmirredb  33615  deg1le0eq0  33656  ply1unit  33658  0mplrim  33698  selvply1rhmlem2  33705  evlextv  33726  mplvrpmrhm  33731  esplyfv1  33753  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  lvecdim0  33791  extdg1b  33851  fldextrspunlsp  33858  irngnzply1  33875  1smat1  33988  ist0cld  34017  qtophaus  34020  reff  34023  locfinreflem  34024  cmpcref  34034  zarcls1  34053  zarclsun  34054  zarclsiin  34055  zarclssn  34057  metider  34078  pstmfval  34080  qqhval2  34166  aean  34428  imambfm  34446  eulerpartlemgvv  34560  orvcgteel  34652  orvclteel  34657  ballotlemsf1o  34698  actfunsnf1o  34788  reprsuc  34799  reprpmtf1o  34810  sconnpi1  35467  brofs2  36305  brifs2  36306  broutsideof2  36350  ttc0elw  36755  bj-abv  37259  irrdiff  37686  ltflcei  37975  poimirlem25  38012  ismblfin  38028  cnambfre  38035  ftc1anclem6  38065  ismndo1  38240  isdrngo2  38325  eqvrelsymb  39057  eqvrelth  39062  lshpnelb  39476  lshpnel2N  39477  lsatspn0  39492  lsatelbN  39498  lsat0cv  39525  lcvexch  39531  lcv1  39533  lkrshp3  39598  lkrpssN  39655  lkrss2N  39661  cvlsupr2  39835  atcvrlln  40012  llncvrlpln  40050  2llnmj  40052  lplncvrlvol  40108  2lplnmj  40114  polcon2bN  40412  pcl0bN  40415  lhpmcvr3  40517  lhpmatb  40523  ltrncoidN  40620  ltrneq3  40700  ltrniotavalbN  41076  cdlemg1cN  41079  diclspsn  41686  dihopelvalcpre  41740  dihord4  41750  dihord  41756  dihmeetlem4preN  41798  dih1dimatlem0  41820  dochsscl  41860  dochoccl  41861  dochord  41862  dochsat  41875  dochshpncl  41876  dochsatshpb  41944  dochshpsat  41946  mapdval4N  42124  mapdsn  42133  hdmap14lem12  42371  hdmapip0  42407  hlhillcs  42450  resuppsinopn  42840  mulgt0b2d  42968  mullt0b1d  42973  mullt0b2d  42974  riccrng  43008  ricdrng  43015  prjspner1  43076  mrefg2  43156  mzpmfp  43196  lzenom  43219  elpell14qr2  43307  elpell1qr2  43317  pellfund14b  43344  congabseq  43419  acongeq  43428  jm2.23  43441  jm2.20nn  43442  jm2.25lem1  43443  wepwsolem  43487  islssfg2  43516  lnmlmic  43533  dfacbasgrp  43553  unielss  43663  rfovcnvf1od  44448  dssmapnvod  44464  ntrclscls00  44510  rfcnpre3  45481  rfcnpre4  45482  ssmapsn  45661  rnmptssbi  45704  infxrgelbrnmpt  45897  xnegre  45909  xrpnf  45928  rexanuz2nf  45935  ioossioobi  45962  iccshift  45963  iocopn  45965  eliccelioc  45966  iooshift  45967  icoopn  45970  qinioo  45980  limcdm0  46063  islptre  46064  islpcn  46082  limcresioolb  46086  climuzlem  46186  climlimsup  46203  liminfgelimsup  46225  liminfgelimsupuz  46231  climliminf  46249  climliminflimsup  46251  climliminflimsup2  46252  xlimpnfxnegmnf  46257  xlimbr  46270  xlimmnfv  46277  xlimpnfv  46281  xlimclim2  46283  dfxlim2v  46290  climresdm  46293  xlimresdm  46302  xlimliminflimsup  46305  fperdvper  46362  itgperiod  46424  fourierdlem32  46582  fourierdlem33  46583  fourierdlem48  46597  fourierdlem49  46598  fourierdlem71  46620  fourierdlem81  46630  preimagelt  47142  preimalegt  47143  smfliminflem  47273  smfliminfmpt  47275  chnsubseqwl  47324  fcoresfob  47535  m1mod0mod1  47823  uhgrimedg  48382  isubgr3stgrlem8  48464  rngcinvALTV  48767  ringcinvALTV  48801  xpco2  49347  fvconstr  49352  fvconstrn0  49353  lubeldm2  49446  glbeldm2  49447  upeu2lem  49518  sectpropd  49527  invpropd  49529  isopropd  49531  cicerALT  49536  cicpropd  49540  up1st2ndb  49677  uobffth  49708  uobeqw  49709  natoppfb  49721  oppc1stflem  49777  fucofulem1  49800  functhinclem1  49934  fullthinc  49940  thincciso4  49947  thinciso  49960  functermclem  49997  termcterm3  50005  termcciso  50006  termcarweu  50018  termfucterm  50034  prstchom2ALT  50054  lanval2  50117  ranval2  50120