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

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

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 395

This theorem is referenced by:  biadanid  819  eqrdav  2729  frsn  5762  funfvbrb  7051  iinpreima  7069  fcdmssb  7122  fnprb  7211  fntpb  7212  fpr2g  7214  nvocnv  7281  fsnex  7283  f1ocnv2d  7661  el2xptp0  8024  1stconst  8088  2ndconst  8089  cnvf1o  8099  fimaproj  8123  tfrlem15  8394  oeeui  8604  ersymb  8719  swoer  8735  erth  8754  boxriin  8936  boxcutc  8937  domunsncan  9074  pw2f1olem  9078  enen1  9119  enen2  9120  domen1  9121  domen2  9122  sdomen1  9123  sdomen2  9124  xpmapenlem  9146  ensymfib  9189  ordiso2  9512  wdomen1  9573  wdomen2  9574  fin23lem26  10322  fpwwe2lem7  10634  r1wunlim  10734  mul2lt0bi  13084  ixxun  13344  xov1plusxeqvd  13479  fzsplit2  13530  fseq1p1m1  13579  elfz2nn0  13596  flflp1  13776  modsubdir  13909  zesq  14193  expnngt1b  14209  hashprg  14359  hashgt0elexb  14366  hashbclem  14415  hashge2el2difb  14447  rereb  15071  rlimclim  15494  iserex  15607  caucvgb  15630  mptfzshft  15728  fsumrev  15729  climcnds  15801  fprodrev  15925  dvdsadd2b  16253  nn0ob  16331  bitsfzo  16380  dfgcd2  16492  dvdsmulgcd  16501  lcmgcdeq  16553  qden1elz  16697  mrcidb  17563  mrieqvlemd  17577  isacs2  17601  cicer  17757  ssclem  17770  issubc3  17803  ffthiso  17884  fuciso  17932  setcmon  18041  setcepi  18042  setcinv  18044  catciso  18065  acsfiindd  18510  issstrmgm  18578  mgmhmf1o  18625  issubmgm2  18628  subsubmgm  18635  resmgmhm2b  18638  issubmnd  18686  mhmf1o  18718  subsubm  18733  resmhm2b  18739  grpinvid1  18912  grpinvid2  18913  subsubg  19065  ssnmz  19082  ghmf1  19160  kerf1ghm  19161  ghmf1o  19162  conjnmzb  19167  subggim  19180  gicsubgen  19193  gass  19206  odf1  19471  gex1  19500  fislw  19534  sylow3lem2  19537  sylow3lem6  19541  lsmdisj2a  19596  lsmdisj2b  19597  efgred2  19662  dmdprdsplit  19958  2nsgsimpgd  20013  simpgnsgbid  20014  ablsimpgd  20027  0unit  20287  irrednegb  20322  rnghmf1o  20343  rhmf1o  20382  subsubrng  20451  subrgunit  20480  subsubrg  20488  isdrng2  20514  issubdrg  20544  islss3  20714  islss4  20717  lspsnel6  20749  lspsneq0b  20768  islmhm2  20793  lmhmf1o  20801  reslmhm2b  20809  lssvs0or  20868  lvecinv  20871  lspsnel4  20882  lspdisjb  20884  islbs2  20912  islbs3  20913  dflidl2  20992  dflidl2rng  21030  rngringbd  21067  prmirredlem  21243  islindf3  21600  lindsmm  21602  lsslindf  21604  lsslinds  21605  issubassa  21640  sraassab  21641  issubassa2  21665  gsumbagdiagOLD  21711  gsumbagdiag  21714  subrgasclcl  21847  matunit  22400  slesolinvbi  22403  en2top  22708  elcls  22797  neindisj2  22847  neiptopnei  22856  neiptopreu  22857  maxlp  22871  neitr  22904  iscncl  22993  cncnp  23004  isreg2  23101  dis2ndc  23184  1stccnp  23186  islly2  23208  dislly  23221  dissnlocfin  23253  kgencmp2  23270  pt1hmeo  23530  xkocnv  23538  t0kq  23542  uffixfr  23647  flimcf  23706  cnpflf2  23724  fclscf  23749  cnextf  23790  utopsnneiplem  23972  isucn2  24004  cfilucfil  24288  psmetutop  24296  restmetu  24299  tngngp2  24389  tngngp  24391  nmoleub  24468  metdseq0  24590  cnheibor  24701  pcophtb  24776  nmoleub2lem  24861  lmmbr  25006  iscfil3  25021  cmetss  25064  cldcss  25189  mbfeqalem2  25391  mbfposb  25402  itg2const2  25491  itgss3  25564  plyco0  25941  dgrlt  26016  ulm2  26133  coseq00topi  26248  coseq0negpitopi  26249  sineq0  26269  relogbcxpb  26528  atans2  26672  xrlimcnp  26709  dchrelbas2  26976  dchrn0  26989  2sqb  27171  nosupbnd2  27455  noinfbnd2  27470  slerec  27557  sltmul2  27862  istrkg2ld  27978  tgcgreqb  27999  tgbtwncomb  28007  trgcgrg  28033  legov  28103  legov2  28104  legov3  28116  hlbtwn  28129  tglineelsb2  28150  tglinecom  28153  colline  28167  mirinv  28184  mirbtwnb  28190  mirbtwnhl  28198  perpcom  28231  isperp2  28233  oppcom  28262  opphllem3  28267  lnopp2hpgb  28281  colopp  28287  colhp  28288  lmieu  28302  iscgra1  28328  dfcgra2  28348  edgnbusgreu  28891  nb3grprlem1  28904  lfgriswlk  29212  eleclclwwlknlem2  29581  clwwlknscsh  29582  clwwlknon1  29617  numclwwlk2lem1  29896  grpoinvid1  30048  grpoinvid2  30049  leopmul  31654  hst1h  31747  eqelbid  31982  diffib  32026  eqsnd  32033  ifnebib  32048  iinabrex  32067  disjabrex  32080  disjabrexf  32081  erbr3b  32113  f1o3d  32118  funimass4f  32128  2ndimaxp  32139  fgreu  32164  fcnvgreu  32165  1stpreimas  32194  fcobij  32214  resf1o  32222  nn0xmulclb  32251  fzsplit3  32272  eliccioo  32364  mgcmntco  32431  dfmgc2lem  32432  dfmgc2  32433  pwrssmgc  32437  mgcf1o  32440  gsumhashmul  32478  ogrpinv0le  32503  ogrpaddltbi  32506  ogrpaddltrbid  32508  ogrpinv0lt  32510  cyc3genpm  32581  isarchi3  32603  prmsimpcyc  32643  isdrng4  32665  qsxpid  32748  dvdsruasso  32764  dvdsrspss  32765  grplsmid  32788  quslsm  32790  nsgmgc  32797  nsgqusf1olem2  32799  nsgqusf1olem3  32800  ghmquskerlem1  32802  ghmqusker  32806  pidlnzb  32814  unitpidl1  32816  elrspunidl  32820  elrspunsn  32821  drngidl  32825  drngidlhash  32826  isprmidlc  32840  prmidl0  32843  qsidom  32847  mxidlirred  32862  mxidlnzrb  32869  qsdrng  32885  ply1scleq  32913  deg1le0eq0  32929  lvecdim0  32979  extdg1b  33031  irngnzply1  33044  1smat1  33082  ist0cld  33111  qtophaus  33114  reff  33117  locfinreflem  33118  cmpcref  33128  zarcls1  33147  zarclsun  33148  zarclsiin  33149  zarclssn  33151  metider  33172  pstmfval  33174  qqhval2  33260  aean  33540  imambfm  33559  eulerpartlemgvv  33673  orvcgteel  33764  orvclteel  33769  ballotlemsf1o  33810  sgn3da  33838  sgnnbi  33842  sgnpbi  33843  sgnmulsgn  33846  sgnmulsgp  33847  actfunsnf1o  33914  reprsuc  33925  reprpmtf1o  33936  sconnpi1  34528  brofs2  35353  brifs2  35354  broutsideof2  35398  bj-abv  36089  irrdiff  36510  ltflcei  36779  poimirlem25  36816  ismblfin  36832  cnambfre  36839  ftc1anclem6  36869  ismndo1  37044  isdrngo2  37129  eqvrelsymb  37779  eqvrelth  37784  lshpnelb  38157  lshpnel2N  38158  lsatspn0  38173  lsatelbN  38179  lsat0cv  38206  lcvexch  38212  lcv1  38214  lkrshp3  38279  lkrpssN  38336  lkrss2N  38342  cvlsupr2  38516  atcvrlln  38694  llncvrlpln  38732  2llnmj  38734  lplncvrlvol  38790  2lplnmj  38796  polcon2bN  39094  pcl0bN  39097  lhpmcvr3  39199  lhpmatb  39205  ltrncoidN  39302  ltrneq3  39382  ltrniotavalbN  39758  cdlemg1cN  39761  diclspsn  40368  dihopelvalcpre  40422  dihord4  40432  dihord  40438  dihmeetlem4preN  40480  dih1dimatlem0  40502  dochsscl  40542  dochoccl  40543  dochord  40544  dochsat  40557  dochshpncl  40558  dochsatshpb  40626  dochshpsat  40628  mapdval4N  40806  mapdsn  40815  hdmap14lem12  41053  hdmapip0  41089  hlhillcs  41136  riccrng  41401  ricdrng  41407  prjspner1  41670  mrefg2  41747  mzpmfp  41787  lzenom  41810  elpell14qr2  41902  elpell1qr2  41912  pellfund14b  41939  congabseq  42015  acongeq  42024  jm2.23  42037  jm2.20nn  42038  jm2.25lem1  42039  wepwsolem  42086  islssfg2  42115  lnmlmic  42132  dfacbasgrp  42152  unielss  42269  rfovcnvf1od  43057  dssmapnvod  43073  ntrclscls00  43119  rfcnpre3  44019  rfcnpre4  44020  rnmptssbi  44263  infxrgelbrnmpt  44462  xnegre  44474  xrpnf  44494  rexanuz2nf  44501  ioossioobi  44528  iccshift  44529  iocopn  44531  eliccelioc  44532  iooshift  44533  icoopn  44536  qinioo  44546  limcdm0  44632  islptre  44633  islpcn  44653  limcresioolb  44657  climuzlem  44757  climlimsup  44774  liminfgelimsup  44796  liminfgelimsupuz  44802  climliminf  44820  climliminflimsup  44822  climliminflimsup2  44823  xlimpnfxnegmnf  44828  xlimbr  44841  xlimmnfv  44848  xlimpnfv  44852  xlimclim2  44854  dfxlim2v  44861  climresdm  44864  xlimresdm  44873  xlimliminflimsup  44876  fperdvper  44933  itgperiod  44995  fourierdlem32  45153  fourierdlem33  45154  fourierdlem48  45168  fourierdlem49  45169  fourierdlem71  45191  fourierdlem81  45201  preimagelt  45713  preimalegt  45714  smfliminflem  45844  smfliminfmpt  45846  fcoresfob  46080  m1mod0mod1  46335  rngcinv  46967  rngcinvALTV  46979  ringcinv  47018  ringcinvALTV  47042  fvconstr  47609  fvconstrn0  47610  lubeldm2  47676  glbeldm2  47677  functhinclem1  47748  fullthinc  47753  thinciso  47767  prstchom2ALT  47786