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  4787  frsn  5712  funfvbrb  6996  iinpreima  7014  fcdmssb  7067  fnprb  7154  fntpb  7155  fpr2g  7157  nvocnv  7227  fsnex  7229  f1ocnv2d  7611  resf1extb  7876  el2xptp0  7980  1stconst  8042  2ndconst  8043  cnvf1o  8053  fimaproj  8077  tfrlem15  8323  oeeui  8530  ersymb  8649  swoer  8666  erth  8689  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  10235  fpwwe2lem7  10548  r1wunlim  10648  mul2lt0bi  13013  ixxun  13277  xov1plusxeqvd  13414  fzsplit2  13465  fseq1p1m1  13514  elfz2nn0  13534  flflp1  13727  modaddb  13829  modsubdir  13863  zesq  14149  expnngt1b  14165  hashprg  14318  hashgt0elexb  14325  hashbclem  14375  hashge2el2difb  14405  rereb  15043  rlimclim  15469  iserex  15580  caucvgb  15603  mptfzshft  15701  fsumrev  15702  climcnds  15774  fprodrev  15900  dvdsadd2b  16233  nn0ob  16311  bitsfzo  16362  dfgcd2  16473  dvdsmulgcd  16483  lcmgcdeq  16539  qden1elz  16684  mrcidb  17538  mrieqvlemd  17552  isacs2  17576  cicer  17730  ssclem  17743  issubc3  17773  ffthiso  17855  fuciso  17902  setcmon  18011  setcepi  18012  setcinv  18014  catciso  18035  acsfiindd  18476  issstrmgm  18578  mgmhmf1o  18625  issubmgm2  18628  subsubmgm  18635  resmgmhm2b  18638  issubmnd  18686  mhmf1o  18721  subsubm  18741  resmhm2b  18747  grpinvid1  18921  grpinvid2  18922  subsubg  19079  ssnmz  19095  ghmf1  19175  kerf1ghm  19176  ghmf1o  19177  conjnmzb  19182  subggim  19195  gicsubgen  19208  ghmqusnsglem1  19209  ghmquskerlem1  19212  ghmqusker  19216  gass  19230  odf1  19491  gex1  19520  fislw  19554  sylow3lem2  19557  sylow3lem6  19561  lsmdisj2a  19616  lsmdisj2b  19617  efgred2  19682  dmdprdsplit  19978  2nsgsimpgd  20033  simpgnsgbid  20034  ablsimpgd  20047  ogrpinv0le  20065  ogrpaddltbi  20068  ogrpaddltrbid  20070  ogrpinv0lt  20072  0unit  20332  irrednegb  20367  rnghmf1o  20388  rhmf1o  20426  subsubrng  20496  subrgunit  20523  subsubrg  20531  rngcinv  20570  ringcinv  20604  isdrng2  20676  issubdrg  20713  islss3  20910  islss4  20913  ellspsn6  20945  lspsneq0b  20964  islmhm2  20990  lmhmf1o  20998  reslmhm2b  21006  lssvs0or  21065  lvecinv  21068  ellspsn4  21079  lspdisjb  21081  islbs2  21109  islbs3  21110  dflidl2rng  21173  rngringbd  21263  prmirredlem  21427  islindf3  21781  lindsmm  21783  lsslindf  21785  lsslinds  21786  issubassa  21822  sraassab  21823  issubassa2  21848  gsumbagdiag  21887  subrgasclcl  22022  ply1scleq  22249  matunit  22622  slesolinvbi  22625  en2top  22929  elcls  23017  neindisj2  23067  neiptopnei  23076  neiptopreu  23077  maxlp  23091  neitr  23124  iscncl  23213  cncnp  23224  isreg2  23321  dis2ndc  23404  1stccnp  23406  islly2  23428  dislly  23441  dissnlocfin  23473  kgencmp2  23490  pt1hmeo  23750  xkocnv  23758  t0kq  23762  uffixfr  23867  flimcf  23926  cnpflf2  23944  fclscf  23969  cnextf  24010  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  25214  iscfil3  25229  cmetss  25272  cldcss  25397  mbfeqalem2  25599  mbfposb  25610  itg2const2  25698  itgss3  25772  plyco0  26153  dgrlt  26228  ulm2  26350  coseq00topi  26467  coseq0negpitopi  26468  sineq0  26489  relogbcxpb  26753  atans2  26897  xrlimcnp  26934  dchrelbas2  27204  dchrn0  27217  2sqb  27399  nosupbnd2  27684  noinfbnd2  27699  lesrec  27795  ltmuls2  28167  elreno2  28491  istrkg2ld  28532  tgcgreqb  28553  tgbtwncomb  28561  trgcgrg  28587  legov  28657  legov2  28658  legov3  28670  hlbtwn  28683  tglineelsb2  28704  tglinecom  28707  colline  28721  mirinv  28738  mirbtwnb  28744  mirbtwnhl  28752  perpcom  28785  isperp2  28787  oppcom  28816  opphllem3  28821  lnopp2hpgb  28835  colopp  28841  colhp  28842  lmieu  28856  iscgra1  28882  dfcgra2  28902  edgnbusgreu  29440  nb3grprlem1  29453  lfgriswlk  29760  eleclclwwlknlem2  30136  clwwlknscsh  30137  clwwlknon1  30172  numclwwlk2lem1  30451  grpoinvid1  30603  grpoinvid2  30604  leopmul  32209  hst1h  32302  eqelbid  32549  diffib  32596  ifnebib  32624  iinabrex  32644  disjabrex  32657  disjabrexf  32658  erbr3b  32695  f1o3d  32704  funimass4f  32715  2ndimaxp  32724  fgreu  32750  fcnvgreu  32751  1stpreimas  32785  fcobij  32799  cocnvf1o  32808  resf1o  32809  nn0xmulclb  32851  fzsplit3  32873  fzo0opth  32883  sgn3da  32915  sgnnbi  32919  sgnpbi  32920  sgnmulsgn  32923  sgnmulsgp  32924  eliccioo  33012  mgcmntco  33076  dfmgc2lem  33077  dfmgc2  33078  pwrssmgc  33082  mgcf1o  33085  mndlrinvb  33107  mndlactfo  33109  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  gsumhashmul  33150  gsumwrd2dccatlem  33159  cyc3genpm  33234  isarchi3  33269  prmsimpcyc  33310  elrgspnsubrunlem1  33329  elrgspnsubrun  33331  domnlcanbOLD  33363  isdrng4  33377  fracerl  33388  qsxpid  33443  dvdsruasso  33466  dvdsruasso2  33467  dvdsrspss  33468  grplsmid  33485  quslsm  33486  nsgmgc  33493  nsgqusf1olem2  33495  nsgqusf1olem3  33496  pidlnzb  33503  unitpidl1  33505  elrspunidl  33509  elrspunsn  33510  drngidl  33514  drngidlhash  33515  isprmidlc  33528  prmidl0  33531  qsidom  33535  mxidlirred  33553  mxidlnzrb  33561  qsdrng  33578  rsprprmprmidlb  33604  rprmirredb  33613  deg1le0eq0  33654  ply1unit  33656  evlextv  33707  mplvrpmrhm  33712  esplyfv1  33727  esplyind  33731  lvecdim0  33763  extdg1b  33824  fldextrspunlsp  33831  irngnzply1  33848  1smat1  33961  ist0cld  33990  qtophaus  33993  reff  33996  locfinreflem  33997  cmpcref  34007  zarcls1  34026  zarclsun  34027  zarclsiin  34028  zarclssn  34030  metider  34051  pstmfval  34053  qqhval2  34139  aean  34401  imambfm  34419  eulerpartlemgvv  34533  orvcgteel  34625  orvclteel  34630  ballotlemsf1o  34671  actfunsnf1o  34761  reprsuc  34772  reprpmtf1o  34783  sconnpi1  35433  brofs2  36271  brifs2  36272  broutsideof2  36316  bj-abv  37107  irrdiff  37531  ltflcei  37809  poimirlem25  37846  ismblfin  37862  cnambfre  37869  ftc1anclem6  37899  ismndo1  38074  isdrngo2  38159  eqvrelsymb  38873  eqvrelth  38878  lshpnelb  39254  lshpnel2N  39255  lsatspn0  39270  lsatelbN  39276  lsat0cv  39303  lcvexch  39309  lcv1  39311  lkrshp3  39376  lkrpssN  39433  lkrss2N  39439  cvlsupr2  39613  atcvrlln  39790  llncvrlpln  39828  2llnmj  39830  lplncvrlvol  39886  2lplnmj  39892  polcon2bN  40190  pcl0bN  40193  lhpmcvr3  40295  lhpmatb  40301  ltrncoidN  40398  ltrneq3  40478  ltrniotavalbN  40854  cdlemg1cN  40857  diclspsn  41464  dihopelvalcpre  41518  dihord4  41528  dihord  41534  dihmeetlem4preN  41576  dih1dimatlem0  41598  dochsscl  41638  dochoccl  41639  dochord  41640  dochsat  41653  dochshpncl  41654  dochsatshpb  41722  dochshpsat  41724  mapdval4N  41902  mapdsn  41911  hdmap14lem12  42149  hdmapip0  42185  hlhillcs  42228  resuppsinopn  42628  mulgt0b2d  42743  mullt0b1d  42748  mullt0b2d  42749  riccrng  42787  ricdrng  42794  prjspner1  42879  mrefg2  42959  mzpmfp  42999  lzenom  43022  elpell14qr2  43114  elpell1qr2  43124  pellfund14b  43151  congabseq  43226  acongeq  43235  jm2.23  43248  jm2.20nn  43249  jm2.25lem1  43250  wepwsolem  43294  islssfg2  43323  lnmlmic  43340  dfacbasgrp  43360  unielss  43470  rfovcnvf1od  44255  dssmapnvod  44271  ntrclscls00  44317  rfcnpre3  45288  rfcnpre4  45289  ssmapsn  45470  rnmptssbi  45514  infxrgelbrnmpt  45708  xnegre  45720  xrpnf  45739  rexanuz2nf  45746  ioossioobi  45773  iccshift  45774  iocopn  45776  eliccelioc  45777  iooshift  45778  icoopn  45781  qinioo  45791  limcdm0  45874  islptre  45875  islpcn  45893  limcresioolb  45897  climuzlem  45997  climlimsup  46014  liminfgelimsup  46036  liminfgelimsupuz  46042  climliminf  46060  climliminflimsup  46062  climliminflimsup2  46063  xlimpnfxnegmnf  46068  xlimbr  46081  xlimmnfv  46088  xlimpnfv  46092  xlimclim2  46094  dfxlim2v  46101  climresdm  46104  xlimresdm  46113  xlimliminflimsup  46116  fperdvper  46173  itgperiod  46235  fourierdlem32  46393  fourierdlem33  46394  fourierdlem48  46408  fourierdlem49  46409  fourierdlem71  46431  fourierdlem81  46441  preimagelt  46953  preimalegt  46954  smfliminflem  47084  smfliminfmpt  47086  chnsubseqwl  47133  fcoresfob  47328  m1mod0mod1  47610  uhgrimedg  48147  isubgr3stgrlem8  48229  rngcinvALTV  48532  ringcinvALTV  48566  xpco2  49112  fvconstr  49117  fvconstrn0  49118  lubeldm2  49211  glbeldm2  49212  upeu2lem  49283  sectpropd  49292  invpropd  49294  isopropd  49296  cicerALT  49301  cicpropd  49305  up1st2ndb  49442  uobffth  49473  uobeqw  49474  natoppfb  49486  oppc1stflem  49542  fucofulem1  49565  functhinclem1  49699  fullthinc  49705  thincciso4  49712  thinciso  49725  functermclem  49762  termcterm3  49770  termcciso  49771  termcarweu  49783  termfucterm  49799  prstchom2ALT  49819  lanval2  49882  ranval2  49885