Theorem impbida 800

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  822  bibiad  839  eqrdav  2735  eqsndOLD  4812  frsn  5747  funfvbrb  7046  iinpreima  7064  fcdmssb  7117  fnprb  7205  fntpb  7206  fpr2g  7208  nvocnv  7279  fsnex  7281  f1ocnv2d  7665  resf1extb  7935  el2xptp0  8040  1stconst  8104  2ndconst  8105  cnvf1o  8115  fimaproj  8139  tfrlem15  8411  oeeui  8619  ersymb  8738  swoer  8755  erth  8775  boxriin  8959  boxcutc  8960  domunsncan  9091  pw2f1olem  9095  enen1  9136  enen2  9137  domen1  9138  domen2  9139  sdomen1  9140  sdomen2  9141  xpmapenlem  9163  ensymfib  9203  ordiso2  9534  wdomen1  9595  wdomen2  9596  fin23lem26  10344  fpwwe2lem7  10656  r1wunlim  10756  mul2lt0bi  13120  ixxun  13383  xov1plusxeqvd  13520  fzsplit2  13571  fseq1p1m1  13620  elfz2nn0  13640  flflp1  13829  modsubdir  13963  zesq  14249  expnngt1b  14265  hashprg  14418  hashgt0elexb  14425  hashbclem  14475  hashge2el2difb  14505  rereb  15144  rlimclim  15567  iserex  15678  caucvgb  15701  mptfzshft  15799  fsumrev  15800  climcnds  15872  fprodrev  15998  dvdsadd2b  16330  nn0ob  16408  bitsfzo  16459  dfgcd2  16570  dvdsmulgcd  16580  lcmgcdeq  16636  qden1elz  16781  mrcidb  17632  mrieqvlemd  17646  isacs2  17670  cicer  17824  ssclem  17837  issubc3  17867  ffthiso  17949  fuciso  17996  setcmon  18105  setcepi  18106  setcinv  18108  catciso  18129  acsfiindd  18568  issstrmgm  18636  mgmhmf1o  18683  issubmgm2  18686  subsubmgm  18693  resmgmhm2b  18696  issubmnd  18744  mhmf1o  18779  subsubm  18799  resmhm2b  18805  grpinvid1  18979  grpinvid2  18980  subsubg  19137  ssnmz  19154  ghmf1  19234  kerf1ghm  19235  ghmf1o  19236  conjnmzb  19241  subggim  19254  gicsubgen  19267  ghmqusnsglem1  19268  ghmquskerlem1  19271  ghmqusker  19275  gass  19289  odf1  19548  gex1  19577  fislw  19611  sylow3lem2  19614  sylow3lem6  19618  lsmdisj2a  19673  lsmdisj2b  19674  efgred2  19739  dmdprdsplit  20035  2nsgsimpgd  20090  simpgnsgbid  20091  ablsimpgd  20104  0unit  20361  irrednegb  20396  rnghmf1o  20417  rhmf1o  20456  subsubrng  20528  subrgunit  20555  subsubrg  20563  rngcinv  20602  ringcinv  20636  isdrng2  20708  issubdrg  20745  islss3  20921  islss4  20924  ellspsn6  20956  lspsneq0b  20975  islmhm2  21001  lmhmf1o  21009  reslmhm2b  21017  lssvs0or  21076  lvecinv  21079  ellspsn4  21090  lspdisjb  21092  islbs2  21120  islbs3  21121  dflidl2rng  21184  rngringbd  21274  prmirredlem  21438  islindf3  21791  lindsmm  21793  lsslindf  21795  lsslinds  21796  issubassa  21832  sraassab  21833  issubassa2  21857  gsumbagdiag  21896  subrgasclcl  22030  ply1scleq  22248  matunit  22621  slesolinvbi  22624  en2top  22928  elcls  23016  neindisj2  23066  neiptopnei  23075  neiptopreu  23076  maxlp  23090  neitr  23123  iscncl  23212  cncnp  23223  isreg2  23320  dis2ndc  23403  1stccnp  23405  islly2  23427  dislly  23440  dissnlocfin  23472  kgencmp2  23489  pt1hmeo  23749  xkocnv  23757  t0kq  23761  uffixfr  23866  flimcf  23925  cnpflf2  23943  fclscf  23968  cnextf  24009  utopsnneiplem  24191  isucn2  24222  cfilucfil  24503  psmetutop  24511  restmetu  24514  tngngp2  24596  tngngp  24598  nmoleub  24675  metdseq0  24799  cnheibor  24910  pcophtb  24985  nmoleub2lem  25070  lmmbr  25215  iscfil3  25230  cmetss  25273  cldcss  25398  mbfeqalem2  25600  mbfposb  25611  itg2const2  25699  itgss3  25773  plyco0  26154  dgrlt  26229  ulm2  26351  coseq00topi  26468  coseq0negpitopi  26469  sineq0  26490  relogbcxpb  26754  atans2  26898  xrlimcnp  26935  dchrelbas2  27205  dchrn0  27218  2sqb  27400  nosupbnd2  27685  noinfbnd2  27700  slerec  27788  sltmul2  28131  istrkg2ld  28444  tgcgreqb  28465  tgbtwncomb  28473  trgcgrg  28499  legov  28569  legov2  28570  legov3  28582  hlbtwn  28595  tglineelsb2  28616  tglinecom  28619  colline  28633  mirinv  28650  mirbtwnb  28656  mirbtwnhl  28664  perpcom  28697  isperp2  28699  oppcom  28728  opphllem3  28733  lnopp2hpgb  28747  colopp  28753  colhp  28754  lmieu  28768  iscgra1  28794  dfcgra2  28814  edgnbusgreu  29351  nb3grprlem1  29364  lfgriswlk  29673  eleclclwwlknlem2  30047  clwwlknscsh  30048  clwwlknon1  30083  numclwwlk2lem1  30362  grpoinvid1  30514  grpoinvid2  30515  leopmul  32120  hst1h  32213  eqelbid  32461  diffib  32507  ifnebib  32535  iinabrex  32555  disjabrex  32568  disjabrexf  32569  erbr3b  32602  f1o3d  32610  funimass4f  32620  2ndimaxp  32629  fgreu  32655  fcnvgreu  32656  1stpreimas  32688  fcobij  32704  resf1o  32712  nn0xmulclb  32753  fzsplit3  32775  fzo0opth  32787  sgn3da  32818  sgnnbi  32822  sgnpbi  32823  sgnmulsgn  32826  sgnmulsgp  32827  eliccioo  32910  mgcmntco  32979  dfmgc2lem  32980  dfmgc2  32981  pwrssmgc  32985  mgcf1o  32988  mndlrinvb  33025  mndlactfo  33027  mndractfo  33029  mndlactf1o  33030  mndractf1o  33031  gsumhashmul  33060  gsumwrd2dccatlem  33065  ogrpinv0le  33088  ogrpaddltbi  33091  ogrpaddltrbid  33093  ogrpinv0lt  33095  cyc3genpm  33168  isarchi3  33190  prmsimpcyc  33230  elrgspnsubrunlem1  33247  elrgspnsubrun  33249  domnlcanbOLD  33280  isdrng4  33294  fracerl  33305  qsxpid  33382  dvdsruasso  33405  dvdsruasso2  33406  dvdsrspss  33407  grplsmid  33424  quslsm  33425  nsgmgc  33432  nsgqusf1olem2  33434  nsgqusf1olem3  33435  pidlnzb  33442  unitpidl1  33444  elrspunidl  33448  elrspunsn  33449  drngidl  33453  drngidlhash  33454  isprmidlc  33467  prmidl0  33470  qsidom  33474  mxidlirred  33492  mxidlnzrb  33500  qsdrng  33517  rsprprmprmidlb  33543  rprmirredb  33552  deg1le0eq0  33591  ply1unit  33593  lvecdim0  33651  extdg1b  33713  fldextrspunlsp  33720  irngnzply1  33737  1smat1  33840  ist0cld  33869  qtophaus  33872  reff  33875  locfinreflem  33876  cmpcref  33886  zarcls1  33905  zarclsun  33906  zarclsiin  33907  zarclssn  33909  metider  33930  pstmfval  33932  qqhval2  34018  aean  34280  imambfm  34299  eulerpartlemgvv  34413  orvcgteel  34505  orvclteel  34510  ballotlemsf1o  34551  actfunsnf1o  34641  reprsuc  34652  reprpmtf1o  34663  sconnpi1  35266  brofs2  36100  brifs2  36101  broutsideof2  36145  bj-abv  36929  irrdiff  37349  ltflcei  37637  poimirlem25  37674  ismblfin  37690  cnambfre  37697  ftc1anclem6  37727  ismndo1  37902  isdrngo2  37987  eqvrelsymb  38629  eqvrelth  38634  lshpnelb  39007  lshpnel2N  39008  lsatspn0  39023  lsatelbN  39029  lsat0cv  39056  lcvexch  39062  lcv1  39064  lkrshp3  39129  lkrpssN  39186  lkrss2N  39192  cvlsupr2  39366  atcvrlln  39544  llncvrlpln  39582  2llnmj  39584  lplncvrlvol  39640  2lplnmj  39646  polcon2bN  39944  pcl0bN  39947  lhpmcvr3  40049  lhpmatb  40055  ltrncoidN  40152  ltrneq3  40232  ltrniotavalbN  40608  cdlemg1cN  40611  diclspsn  41218  dihopelvalcpre  41272  dihord4  41282  dihord  41288  dihmeetlem4preN  41330  dih1dimatlem0  41352  dochsscl  41392  dochoccl  41393  dochord  41394  dochsat  41407  dochshpncl  41408  dochsatshpb  41476  dochshpsat  41478  mapdval4N  41656  mapdsn  41665  hdmap14lem12  41903  hdmapip0  41939  hlhillcs  41982  resuppsinopn  42381  riccrng  42520  ricdrng  42527  prjspner1  42624  mrefg2  42705  mzpmfp  42745  lzenom  42768  elpell14qr2  42860  elpell1qr2  42870  pellfund14b  42897  congabseq  42973  acongeq  42982  jm2.23  42995  jm2.20nn  42996  jm2.25lem1  42997  wepwsolem  43041  islssfg2  43070  lnmlmic  43087  dfacbasgrp  43107  unielss  43217  rfovcnvf1od  44003  dssmapnvod  44019  ntrclscls00  44065  rfcnpre3  45037  rfcnpre4  45038  ssmapsn  45220  rnmptssbi  45264  infxrgelbrnmpt  45461  xnegre  45473  xrpnf  45492  rexanuz2nf  45499  ioossioobi  45526  iccshift  45527  iocopn  45529  eliccelioc  45530  iooshift  45531  icoopn  45534  qinioo  45544  limcdm0  45627  islptre  45628  islpcn  45648  limcresioolb  45652  climuzlem  45752  climlimsup  45769  liminfgelimsup  45791  liminfgelimsupuz  45797  climliminf  45815  climliminflimsup  45817  climliminflimsup2  45818  xlimpnfxnegmnf  45823  xlimbr  45836  xlimmnfv  45843  xlimpnfv  45847  xlimclim2  45849  dfxlim2v  45856  climresdm  45859  xlimresdm  45868  xlimliminflimsup  45871  fperdvper  45928  itgperiod  45990  fourierdlem32  46148  fourierdlem33  46149  fourierdlem48  46163  fourierdlem49  46164  fourierdlem71  46186  fourierdlem81  46196  preimagelt  46708  preimalegt  46709  smfliminflem  46839  smfliminfmpt  46841  fcoresfob  47081  m1mod0mod1  47363  uhgrimedg  47884  isubgr3stgrlem8  47965  rngcinvALTV  48231  ringcinvALTV  48265  fvconstr  48818  fvconstrn0  48819  lubeldm2  48910  glbeldm2  48911  upeu2lem  48978  sectpropd  48984  invpropd  48986  isopropd  48988  cicerALT  48993  cicpropd  48997  up1st2ndb  49101  fucofulem1  49201  functhinclem1  49310  fullthinc  49316  thincciso4  49323  thinciso  49336  functermclem  49372  termcterm3  49380  termcciso  49381  termcarweu  49393  prstchom2ALT  49421  lanval2  49482  ranval2  49485