Theorem impbida 801

Description: Deduce an equivalence from two implications. Variant of impbid 215. (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 416	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 416	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 215	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biadanid  823  eqrdav  2736  frsn  5636  funfvbrb  6871  iinpreima  6889  frnssb  6938  fnprb  7024  fntpb  7025  fpr2g  7027  nvocnv  7092  fsnex  7093  f1ocnv2d  7458  el2xptp0  7808  1stconst  7868  2ndconst  7869  cnvf1o  7879  fimaproj  7902  tfrlem15  8128  oeeui  8330  ersymb  8405  swoer  8421  erth  8440  boxriin  8621  boxcutc  8622  domunsncan  8745  pw2f1olem  8749  enen1  8786  enen2  8787  domen1  8788  domen2  8789  sdomen1  8790  sdomen2  8791  xpmapenlem  8813  ensymfib  8862  ordiso2  9131  wdomen1  9192  wdomen2  9193  fin23lem26  9939  fpwwe2lem7  10251  r1wunlim  10351  mul2lt0bi  12692  ixxun  12951  xov1plusxeqvd  13086  fzsplit2  13137  fseq1p1m1  13186  elfz2nn0  13203  flflp1  13382  modsubdir  13513  zesq  13793  expnngt1b  13809  hashprg  13962  hashgt0elexb  13969  hashbclem  14016  hashge2el2difb  14048  rereb  14683  rlimclim  15107  iserex  15220  caucvgb  15243  mptfzshft  15342  fsumrev  15343  climcnds  15415  fprodrev  15539  dvdsadd2b  15867  nn0ob  15945  bitsfzo  15994  dfgcd2  16106  dvdsmulgcd  16117  lcmgcdeq  16169  qden1elz  16313  mrcidb  17118  mrieqvlemd  17132  isacs2  17156  cicer  17311  ssclem  17324  issubc3  17355  ffthiso  17436  fuciso  17484  setcmon  17593  setcepi  17594  setcinv  17596  catciso  17617  acsfiindd  18059  issstrmgm  18125  issubmnd  18200  mhmf1o  18228  subsubm  18243  resmhm2b  18249  grpinvid1  18418  grpinvid2  18419  subsubg  18566  ssnmz  18582  ghmf1  18651  ghmf1o  18652  conjnmzb  18657  subggim  18670  gicsubgen  18682  gass  18695  odf1  18953  gex1  18980  fislw  19014  sylow3lem2  19017  sylow3lem6  19021  lsmdisj2a  19077  lsmdisj2b  19078  efgred2  19143  dmdprdsplit  19434  2nsgsimpgd  19489  simpgnsgbid  19490  ablsimpgd  19503  0unit  19698  irrednegb  19729  rhmf1o  19752  kerf1ghm  19763  isdrng2  19777  subrgunit  19818  issubdrg  19825  subsubrg  19826  islss3  19996  islss4  19999  lspsnel6  20031  lspsneq0b  20050  islmhm2  20075  lmhmf1o  20083  reslmhm2b  20091  lssvs0or  20147  lvecinv  20150  lspsnel4  20161  lspdisjb  20163  islbs2  20191  islbs3  20192  prmirredlem  20459  islindf3  20788  lindsmm  20790  lsslindf  20792  lsslinds  20793  issubassa  20828  issubassa2  20852  gsumbagdiagOLD  20898  gsumbagdiag  20901  subrgasclcl  21025  matunit  21575  slesolinvbi  21578  en2top  21882  elcls  21970  neindisj2  22020  neiptopnei  22029  neiptopreu  22030  maxlp  22044  neitr  22077  iscncl  22166  cncnp  22177  isreg2  22274  dis2ndc  22357  1stccnp  22359  islly2  22381  dislly  22394  dissnlocfin  22426  kgencmp2  22443  pt1hmeo  22703  xkocnv  22711  t0kq  22715  uffixfr  22820  flimcf  22879  cnpflf2  22897  fclscf  22922  cnextf  22963  utopsnneiplem  23145  isucn2  23176  cfilucfil  23457  psmetutop  23465  restmetu  23468  tngngp2  23550  tngngp  23552  nmoleub  23629  metdseq0  23751  cnheibor  23852  pcophtb  23926  nmoleub2lem  24011  lmmbr  24155  iscfil3  24170  cmetss  24213  cldcss  24338  mbfeqalem2  24539  mbfposb  24550  itg2const2  24639  itgss3  24712  plyco0  25086  dgrlt  25160  ulm2  25277  coseq00topi  25392  coseq0negpitopi  25393  sineq0  25413  relogbcxpb  25670  atans2  25814  xrlimcnp  25851  dchrelbas2  26118  dchrn0  26131  2sqb  26313  istrkg2ld  26551  tgcgreqb  26572  tgbtwncomb  26580  trgcgrg  26606  legov  26676  legov2  26677  legov3  26689  hlbtwn  26702  tglineelsb2  26723  tglinecom  26726  colline  26740  mirinv  26757  mirbtwnb  26763  mirbtwnhl  26771  perpcom  26804  isperp2  26806  oppcom  26835  opphllem3  26840  lnopp2hpgb  26854  colopp  26860  colhp  26861  lmieu  26875  iscgra1  26901  dfcgra2  26921  edgnbusgreu  27455  nb3grprlem1  27468  lfgriswlk  27776  eleclclwwlknlem2  28144  clwwlknscsh  28145  clwwlknon1  28180  numclwwlk2lem1  28459  grpoinvid1  28609  grpoinvid2  28610  leopmul  30215  hst1h  30308  diffib  30588  eqsnd  30596  iinabrex  30627  disjabrex  30640  disjabrexf  30641  erbr3b  30676  f1o3d  30681  funimass4f  30691  2ndimaxp  30703  fgreu  30729  fcnvgreu  30730  1stpreimas  30758  fcobij  30777  resf1o  30785  nn0xmulclb  30814  fzsplit3  30835  eliccioo  30925  mgcmntco  30991  dfmgc2lem  30992  dfmgc2  30993  pwrssmgc  30997  mgcf1o  31000  gsumhashmul  31035  ogrpinv0le  31060  ogrpaddltbi  31063  ogrpaddltrbid  31065  ogrpinv0lt  31067  cyc3genpm  31138  isarchi3  31160  prmsimpcyc  31200  qsxpid  31272  grplsmid  31306  quslsm  31307  nsgmgc  31311  nsgqusf1olem2  31313  nsgqusf1olem3  31314  elrspunidl  31320  isprmidlc  31337  prmidl0  31340  qsidom  31344  mxidlnzrb  31358  ply1scleq  31382  lvecdim0  31404  extdg1b  31453  1smat1  31468  ist0cld  31497  qtophaus  31500  reff  31503  locfinreflem  31504  cmpcref  31514  zarcls1  31533  zarclsun  31534  zarclsiin  31535  zarclssn  31537  metider  31558  pstmfval  31560  qqhval2  31644  aean  31924  imambfm  31941  eulerpartlemgvv  32055  orvcgteel  32146  orvclteel  32151  ballotlemsf1o  32192  sgn3da  32220  sgnnbi  32224  sgnpbi  32225  sgnmulsgn  32228  sgnmulsgp  32229  actfunsnf1o  32296  reprsuc  32307  reprpmtf1o  32318  sconnpi1  32914  nosupbnd2  33656  noinfbnd2  33671  slerec  33750  brofs2  34116  brifs2  34117  broutsideof2  34161  bj-abv  34828  irrdiff  35231  ltflcei  35502  poimirlem25  35539  ismblfin  35555  cnambfre  35562  ftc1anclem6  35592  ismndo1  35768  isdrngo2  35853  eqvrelsymb  36456  eqvrelth  36461  lshpnelb  36735  lshpnel2N  36736  lsatspn0  36751  lsatelbN  36757  lsat0cv  36784  lcvexch  36790  lcv1  36792  lkrshp3  36857  lkrpssN  36914  lkrss2N  36920  cvlsupr2  37094  atcvrlln  37271  llncvrlpln  37309  2llnmj  37311  lplncvrlvol  37367  2lplnmj  37373  polcon2bN  37671  pcl0bN  37674  lhpmcvr3  37776  lhpmatb  37782  ltrncoidN  37879  ltrneq3  37959  ltrniotavalbN  38335  cdlemg1cN  38338  diclspsn  38945  dihopelvalcpre  38999  dihord4  39009  dihord  39015  dihmeetlem4preN  39057  dih1dimatlem0  39079  dochsscl  39119  dochoccl  39120  dochord  39121  dochsat  39134  dochshpncl  39135  dochsatshpb  39203  dochshpsat  39205  mapdval4N  39383  mapdsn  39392  hdmap14lem12  39630  hdmapip0  39666  hlhillcs  39709  prjspner1  40171  mrefg2  40232  mzpmfp  40272  lzenom  40295  elpell14qr2  40387  elpell1qr2  40397  pellfund14b  40424  congabseq  40499  acongeq  40508  jm2.23  40521  jm2.20nn  40522  jm2.25lem1  40523  wepwsolem  40570  islssfg2  40599  lnmlmic  40616  dfacbasgrp  40636  rfovcnvf1od  41289  dssmapnvod  41305  ntrclscls00  41353  rfcnpre3  42249  rfcnpre4  42250  rnmptssbi  42479  infxrgelbrnmpt  42669  xnegre  42681  xrpnf  42701  ioossioobi  42730  iccshift  42731  iocopn  42733  eliccelioc  42734  iooshift  42735  icoopn  42738  qinioo  42748  limcdm0  42834  islptre  42835  islpcn  42855  limcresioolb  42859  climuzlem  42959  climlimsup  42976  liminfgelimsup  42998  liminfgelimsupuz  43004  climliminf  43022  climliminflimsup  43024  climliminflimsup2  43025  xlimpnfxnegmnf  43030  xlimbr  43043  xlimmnfv  43050  xlimpnfv  43054  xlimclim2  43056  dfxlim2v  43063  climresdm  43066  xlimresdm  43075  xlimliminflimsup  43078  fperdvper  43135  itgperiod  43197  fourierdlem32  43355  fourierdlem33  43356  fourierdlem48  43370  fourierdlem49  43371  fourierdlem71  43393  fourierdlem81  43403  preimagelt  43911  preimalegt  43912  smfliminflem  44035  smfliminfmpt  44037  fcoresfob  44238  m1mod0mod1  44494  mgmhmf1o  45014  issubmgm2  45017  subsubmgm  45024  resmgmhm2b  45027  rnghmf1o  45134  rngcinv  45212  rngcinvALTV  45224  ringcinv  45263  ringcinvALTV  45287  fvconstr  45856  fvconstrn0  45857  lubeldm2  45923  glbeldm2  45924  functhinclem1  45995  fullthinc  46000  thinciso  46014  prstchom2ALT  46031