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 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  821  eqrdav  2725  eqsndOLD  4840  frsn  5771  funfvbrb  7066  iinpreima  7084  fcdmssb  7138  fnprb  7227  fntpb  7228  fpr2g  7230  nvocnv  7297  fsnex  7299  f1ocnv2d  7681  el2xptp0  8052  1stconst  8116  2ndconst  8117  cnvf1o  8127  fimaproj  8151  tfrlem15  8424  oeeui  8634  ersymb  8750  swoer  8767  erth  8787  boxriin  8971  boxcutc  8972  domunsncan  9112  pw2f1olem  9116  enen1  9157  enen2  9158  domen1  9159  domen2  9160  sdomen1  9161  sdomen2  9162  xpmapenlem  9184  ensymfib  9223  ordiso2  9560  wdomen1  9621  wdomen2  9622  fin23lem26  10370  fpwwe2lem7  10682  r1wunlim  10782  mul2lt0bi  13136  ixxun  13396  xov1plusxeqvd  13531  fzsplit2  13582  fseq1p1m1  13631  elfz2nn0  13648  flflp1  13829  modsubdir  13962  zesq  14245  expnngt1b  14261  hashprg  14414  hashgt0elexb  14421  hashbclem  14471  hashge2el2difb  14503  rereb  15127  rlimclim  15550  iserex  15663  caucvgb  15686  mptfzshft  15784  fsumrev  15785  climcnds  15857  fprodrev  15981  dvdsadd2b  16310  nn0ob  16388  bitsfzo  16437  dfgcd2  16549  dvdsmulgcd  16559  lcmgcdeq  16615  qden1elz  16761  mrcidb  17630  mrieqvlemd  17644  isacs2  17668  cicer  17824  ssclem  17837  issubc3  17870  ffthiso  17953  fuciso  18002  setcmon  18111  setcepi  18112  setcinv  18114  catciso  18135  acsfiindd  18580  issstrmgm  18648  mgmhmf1o  18695  issubmgm2  18698  subsubmgm  18705  resmgmhm2b  18708  issubmnd  18756  mhmf1o  18788  subsubm  18808  resmhm2b  18814  grpinvid1  18988  grpinvid2  18989  subsubg  19145  ssnmz  19162  ghmf1  19242  kerf1ghm  19243  ghmf1o  19244  conjnmzb  19249  subggim  19262  gicsubgen  19275  ghmqusnsglem1  19276  ghmquskerlem1  19279  ghmqusker  19283  gass  19297  odf1  19562  gex1  19591  fislw  19625  sylow3lem2  19628  sylow3lem6  19632  lsmdisj2a  19687  lsmdisj2b  19688  efgred2  19753  dmdprdsplit  20049  2nsgsimpgd  20104  simpgnsgbid  20105  ablsimpgd  20118  0unit  20380  irrednegb  20415  rnghmf1o  20436  rhmf1o  20475  subsubrng  20547  subrgunit  20576  subsubrg  20584  rngcinv  20617  ringcinv  20651  isdrng2  20723  issubdrg  20761  islss3  20938  islss4  20941  ellspsn6  20973  lspsneq0b  20992  islmhm2  21018  lmhmf1o  21026  reslmhm2b  21034  lssvs0or  21093  lvecinv  21096  ellspsn4  21107  lspdisjb  21109  islbs2  21137  islbs3  21138  dflidl2rng  21209  rngringbd  21299  prmirredlem  21464  islindf3  21826  lindsmm  21828  lsslindf  21830  lsslinds  21831  issubassa  21866  sraassab  21867  issubassa2  21891  gsumbagdiagOLD  21939  gsumbagdiag  21942  subrgasclcl  22082  ply1scleq  22299  matunit  22674  slesolinvbi  22677  en2top  22982  elcls  23071  neindisj2  23121  neiptopnei  23130  neiptopreu  23131  maxlp  23145  neitr  23178  iscncl  23267  cncnp  23278  isreg2  23375  dis2ndc  23458  1stccnp  23460  islly2  23482  dislly  23495  dissnlocfin  23527  kgencmp2  23544  pt1hmeo  23804  xkocnv  23812  t0kq  23816  uffixfr  23921  flimcf  23980  cnpflf2  23998  fclscf  24023  cnextf  24064  utopsnneiplem  24246  isucn2  24278  cfilucfil  24562  psmetutop  24570  restmetu  24573  tngngp2  24663  tngngp  24665  nmoleub  24742  metdseq0  24864  cnheibor  24975  pcophtb  25050  nmoleub2lem  25135  lmmbr  25280  iscfil3  25295  cmetss  25338  cldcss  25463  mbfeqalem2  25665  mbfposb  25676  itg2const2  25765  itgss3  25838  plyco0  26222  dgrlt  26297  ulm2  26417  coseq00topi  26533  coseq0negpitopi  26534  sineq0  26554  relogbcxpb  26818  atans2  26962  xrlimcnp  26999  dchrelbas2  27269  dchrn0  27282  2sqb  27464  nosupbnd2  27749  noinfbnd2  27764  slerec  27852  sltmul2  28175  istrkg2ld  28390  tgcgreqb  28411  tgbtwncomb  28419  trgcgrg  28445  legov  28515  legov2  28516  legov3  28528  hlbtwn  28541  tglineelsb2  28562  tglinecom  28565  colline  28579  mirinv  28596  mirbtwnb  28602  mirbtwnhl  28610  perpcom  28643  isperp2  28645  oppcom  28674  opphllem3  28679  lnopp2hpgb  28693  colopp  28699  colhp  28700  lmieu  28714  iscgra1  28740  dfcgra2  28760  edgnbusgreu  29306  nb3grprlem1  29319  lfgriswlk  29628  eleclclwwlknlem2  29997  clwwlknscsh  29998  clwwlknon1  30033  numclwwlk2lem1  30312  grpoinvid1  30464  grpoinvid2  30465  leopmul  32070  hst1h  32163  bibiad  32390  eqelbid  32406  diffib  32451  ifnebib  32472  iinabrex  32491  disjabrex  32504  disjabrexf  32505  erbr3b  32539  f1o3d  32546  funimass4f  32556  2ndimaxp  32566  fgreu  32591  fcnvgreu  32592  1stpreimas  32619  fcobij  32638  resf1o  32646  nn0xmulclb  32677  fzsplit3  32698  fzo0opth  32709  eliccioo  32794  mgcmntco  32866  dfmgc2lem  32867  dfmgc2  32868  pwrssmgc  32872  mgcf1o  32875  gsumhashmul  32927  ogrpinv0le  32952  ogrpaddltbi  32955  ogrpaddltrbid  32957  ogrpinv0lt  32959  cyc3genpm  33032  isarchi3  33054  prmsimpcyc  33094  domnlcanbOLD  33135  isdrng4  33149  fracerl  33158  qsxpid  33239  dvdsruasso  33262  dvdsruasso2  33263  dvdsrspss  33264  grplsmid  33281  quslsm  33282  nsgmgc  33289  nsgqusf1olem2  33291  nsgqusf1olem3  33292  pidlnzb  33299  unitpidl1  33301  elrspunidl  33305  elrspunsn  33306  drngidl  33310  drngidlhash  33311  isprmidlc  33324  prmidl0  33327  qsidom  33331  mxidlirred  33349  mxidlnzrb  33357  qsdrng  33374  rsprprmprmidlb  33400  rprmirredb  33409  deg1le0eq0  33447  ply1unit  33449  lvecdim0  33503  extdg1b  33555  irngnzply1  33569  1smat1  33621  ist0cld  33650  qtophaus  33653  reff  33656  locfinreflem  33657  cmpcref  33667  zarcls1  33686  zarclsun  33687  zarclsiin  33688  zarclssn  33690  metider  33711  pstmfval  33713  qqhval2  33799  aean  34079  imambfm  34098  eulerpartlemgvv  34212  orvcgteel  34303  orvclteel  34308  ballotlemsf1o  34349  sgn3da  34377  sgnnbi  34381  sgnpbi  34382  sgnmulsgn  34385  sgnmulsgp  34386  actfunsnf1o  34452  reprsuc  34463  reprpmtf1o  34474  sconnpi1  35069  brofs2  35903  brifs2  35904  broutsideof2  35948  bj-abv  36614  irrdiff  37035  ltflcei  37311  poimirlem25  37348  ismblfin  37364  cnambfre  37371  ftc1anclem6  37401  ismndo1  37576  isdrngo2  37661  eqvrelsymb  38306  eqvrelth  38311  lshpnelb  38684  lshpnel2N  38685  lsatspn0  38700  lsatelbN  38706  lsat0cv  38733  lcvexch  38739  lcv1  38741  lkrshp3  38806  lkrpssN  38863  lkrss2N  38869  cvlsupr2  39043  atcvrlln  39221  llncvrlpln  39259  2llnmj  39261  lplncvrlvol  39317  2lplnmj  39323  polcon2bN  39621  pcl0bN  39624  lhpmcvr3  39726  lhpmatb  39732  ltrncoidN  39829  ltrneq3  39909  ltrniotavalbN  40285  cdlemg1cN  40288  diclspsn  40895  dihopelvalcpre  40949  dihord4  40959  dihord  40965  dihmeetlem4preN  41007  dih1dimatlem0  41029  dochsscl  41069  dochoccl  41070  dochord  41071  dochsat  41084  dochshpncl  41085  dochsatshpb  41153  dochshpsat  41155  mapdval4N  41333  mapdsn  41342  hdmap14lem12  41580  hdmapip0  41616  hlhillcs  41663  riccrng  42192  ricdrng  42199  prjspner1  42296  mrefg2  42382  mzpmfp  42422  lzenom  42445  elpell14qr2  42537  elpell1qr2  42547  pellfund14b  42574  congabseq  42650  acongeq  42659  jm2.23  42672  jm2.20nn  42673  jm2.25lem1  42674  wepwsolem  42721  islssfg2  42750  lnmlmic  42767  dfacbasgrp  42787  unielss  42901  rfovcnvf1od  43689  dssmapnvod  43705  ntrclscls00  43751  rfcnpre3  44650  rfcnpre4  44651  rnmptssbi  44888  infxrgelbrnmpt  45087  xnegre  45099  xrpnf  45119  rexanuz2nf  45126  ioossioobi  45153  iccshift  45154  iocopn  45156  eliccelioc  45157  iooshift  45158  icoopn  45161  qinioo  45171  limcdm0  45257  islptre  45258  islpcn  45278  limcresioolb  45282  climuzlem  45382  climlimsup  45399  liminfgelimsup  45421  liminfgelimsupuz  45427  climliminf  45445  climliminflimsup  45447  climliminflimsup2  45448  xlimpnfxnegmnf  45453  xlimbr  45466  xlimmnfv  45473  xlimpnfv  45477  xlimclim2  45479  dfxlim2v  45486  climresdm  45489  xlimresdm  45498  xlimliminflimsup  45501  fperdvper  45558  itgperiod  45620  fourierdlem32  45778  fourierdlem33  45779  fourierdlem48  45793  fourierdlem49  45794  fourierdlem71  45816  fourierdlem81  45826  preimagelt  46338  preimalegt  46339  smfliminflem  46469  smfliminfmpt  46471  fcoresfob  46705  m1mod0mod1  46959  uspgrimprop  47470  rngcinvALTV  47671  ringcinvALTV  47705  fvconstr  48241  fvconstrn0  48242  lubeldm2  48308  glbeldm2  48309  functhinclem1  48380  fullthinc  48385  thinciso  48399  prstchom2ALT  48418