Theorem impbida 801

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  823  bibiad  840  eqrdav  2736  eqsndOLD  4775  frsn  5710  funfvbrb  6995  iinpreima  7013  fcdmssb  7066  fnprb  7154  fntpb  7155  fpr2g  7157  nvocnv  7227  fsnex  7229  f1ocnv2d  7611  resf1extb  7876  el2xptp0  7980  1stconst  8041  2ndconst  8042  cnvf1o  8052  fimaproj  8076  tfrlem15  8322  oeeui  8529  ersymb  8649  swoer  8666  erth  8689  boxriin  8879  boxcutc  8880  domunsncan  9006  pw2f1olem  9010  enen1  9046  enen2  9047  domen1  9048  domen2  9049  sdomen1  9050  sdomen2  9051  xpmapenlem  9073  ensymfib  9109  ordiso2  9421  wdomen1  9482  wdomen2  9483  fin23lem26  10236  fpwwe2lem7  10549  r1wunlim  10649  mul2lt0bi  13014  ixxun  13278  xov1plusxeqvd  13415  fzsplit2  13466  fseq1p1m1  13515  elfz2nn0  13535  flflp1  13728  modaddb  13830  modsubdir  13864  zesq  14150  expnngt1b  14166  hashprg  14319  hashgt0elexb  14326  hashbclem  14376  hashge2el2difb  14406  rereb  15044  rlimclim  15470  iserex  15581  caucvgb  15604  mptfzshft  15702  fsumrev  15703  climcnds  15775  fprodrev  15901  dvdsadd2b  16234  nn0ob  16312  bitsfzo  16363  dfgcd2  16474  dvdsmulgcd  16484  lcmgcdeq  16540  qden1elz  16685  mrcidb  17539  mrieqvlemd  17553  isacs2  17577  cicer  17731  ssclem  17744  issubc3  17774  ffthiso  17856  fuciso  17903  setcmon  18012  setcepi  18013  setcinv  18015  catciso  18036  acsfiindd  18477  issstrmgm  18579  mgmhmf1o  18626  issubmgm2  18629  subsubmgm  18636  resmgmhm2b  18639  issubmnd  18687  mhmf1o  18722  subsubm  18742  resmhm2b  18748  grpinvid1  18925  grpinvid2  18926  subsubg  19083  ssnmz  19099  ghmf1  19179  kerf1ghm  19180  ghmf1o  19181  conjnmzb  19186  subggim  19199  gicsubgen  19212  ghmqusnsglem1  19213  ghmquskerlem1  19216  ghmqusker  19220  gass  19234  odf1  19495  gex1  19524  fislw  19558  sylow3lem2  19561  sylow3lem6  19565  lsmdisj2a  19620  lsmdisj2b  19621  efgred2  19686  dmdprdsplit  19982  2nsgsimpgd  20037  simpgnsgbid  20038  ablsimpgd  20051  ogrpinv0le  20069  ogrpaddltbi  20072  ogrpaddltrbid  20074  ogrpinv0lt  20076  0unit  20334  irrednegb  20369  rnghmf1o  20390  rhmf1o  20428  subsubrng  20498  subrgunit  20525  subsubrg  20533  rngcinv  20572  ringcinv  20606  isdrng2  20678  issubdrg  20715  islss3  20912  islss4  20915  ellspsn6  20947  lspsneq0b  20966  islmhm2  20992  lmhmf1o  21000  reslmhm2b  21008  lssvs0or  21067  lvecinv  21070  ellspsn4  21081  lspdisjb  21083  islbs2  21111  islbs3  21112  dflidl2rng  21175  rngringbd  21265  prmirredlem  21429  islindf3  21783  lindsmm  21785  lsslindf  21787  lsslinds  21788  issubassa  21824  sraassab  21825  issubassa2  21849  gsumbagdiag  21888  subrgasclcl  22023  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  24190  isucn2  24221  cfilucfil  24502  psmetutop  24510  restmetu  24513  tngngp2  24595  tngngp  24597  nmoleub  24674  metdseq0  24798  cnheibor  24900  pcophtb  24974  nmoleub2lem  25059  lmmbr  25203  iscfil3  25218  cmetss  25261  cldcss  25386  mbfeqalem2  25587  mbfposb  25598  itg2const2  25686  itgss3  25760  plyco0  26138  dgrlt  26212  ulm2  26334  coseq00topi  26451  coseq0negpitopi  26452  sineq0  26473  relogbcxpb  26737  atans2  26881  xrlimcnp  26918  dchrelbas2  27188  dchrn0  27201  2sqb  27383  nosupbnd2  27668  noinfbnd2  27683  lesrec  27779  ltmuls2  28151  elreno2  28475  istrkg2ld  28516  tgcgreqb  28537  tgbtwncomb  28545  trgcgrg  28571  legov  28641  legov2  28642  legov3  28654  hlbtwn  28667  tglineelsb2  28688  tglinecom  28691  colline  28705  mirinv  28722  mirbtwnb  28728  mirbtwnhl  28736  perpcom  28769  isperp2  28771  oppcom  28800  opphllem3  28805  lnopp2hpgb  28819  colopp  28825  colhp  28826  lmieu  28840  iscgra1  28866  dfcgra2  28886  edgnbusgreu  29424  nb3grprlem1  29437  lfgriswlk  29744  eleclclwwlknlem2  30120  clwwlknscsh  30121  clwwlknon1  30156  numclwwlk2lem1  30435  grpoinvid1  30588  grpoinvid2  30589  leopmul  32194  hst1h  32287  eqelbid  32533  diffib  32580  ifnebib  32608  iinabrex  32628  disjabrex  32641  disjabrexf  32642  erbr3b  32679  f1o3d  32688  funimass4f  32699  2ndimaxp  32708  fgreu  32733  fcnvgreu  32734  1stpreimas  32768  fcobij  32782  cocnvf1o  32791  resf1o  32792  nn0xmulclb  32834  fzsplit3  32856  fzo0opth  32866  sgn3da  32898  sgnnbi  32902  sgnpbi  32903  sgnmulsgn  32906  sgnmulsgp  32907  eliccioo  32995  mgcmntco  33059  dfmgc2lem  33060  dfmgc2  33061  pwrssmgc  33065  mgcf1o  33068  mndlrinvb  33090  mndlactfo  33092  mndractfo  33094  mndlactf1o  33095  mndractf1o  33096  gsumhashmul  33133  gsumwrd2dccatlem  33143  cyc3genpm  33218  isarchi3  33253  prmsimpcyc  33294  elrgspnsubrunlem1  33313  elrgspnsubrun  33315  domnlcanbOLD  33347  isdrng4  33361  fracerl  33372  qsxpid  33427  dvdsruasso  33450  dvdsruasso2  33451  dvdsrspss  33452  grplsmid  33469  quslsm  33470  nsgmgc  33477  nsgqusf1olem2  33479  nsgqusf1olem3  33480  pidlnzb  33487  unitpidl1  33489  elrspunidl  33493  elrspunsn  33494  drngidl  33498  drngidlhash  33499  isprmidlc  33512  prmidl0  33515  qsidom  33519  mxidlirred  33537  mxidlnzrb  33545  qsdrng  33562  rsprprmprmidlb  33588  rprmirredb  33597  deg1le0eq0  33638  ply1unit  33640  evlextv  33691  mplvrpmrhm  33696  esplyfv1  33718  esplyfval1  33722  esplyfvaln  33723  esplyind  33724  lvecdim0  33756  extdg1b  33817  fldextrspunlsp  33824  irngnzply1  33841  1smat1  33954  ist0cld  33983  qtophaus  33986  reff  33989  locfinreflem  33990  cmpcref  34000  zarcls1  34019  zarclsun  34020  zarclsiin  34021  zarclssn  34023  metider  34044  pstmfval  34046  qqhval2  34132  aean  34394  imambfm  34412  eulerpartlemgvv  34526  orvcgteel  34618  orvclteel  34623  ballotlemsf1o  34664  actfunsnf1o  34754  reprsuc  34765  reprpmtf1o  34776  sconnpi1  35427  brofs2  36265  brifs2  36266  broutsideof2  36310  ttc0elw  36715  bj-abv  37211  irrdiff  37638  ltflcei  37920  poimirlem25  37957  ismblfin  37973  cnambfre  37980  ftc1anclem6  38010  ismndo1  38185  isdrngo2  38270  eqvrelsymb  39002  eqvrelth  39007  lshpnelb  39421  lshpnel2N  39422  lsatspn0  39437  lsatelbN  39443  lsat0cv  39470  lcvexch  39476  lcv1  39478  lkrshp3  39543  lkrpssN  39600  lkrss2N  39606  cvlsupr2  39780  atcvrlln  39957  llncvrlpln  39995  2llnmj  39997  lplncvrlvol  40053  2lplnmj  40059  polcon2bN  40357  pcl0bN  40360  lhpmcvr3  40462  lhpmatb  40468  ltrncoidN  40565  ltrneq3  40645  ltrniotavalbN  41021  cdlemg1cN  41024  diclspsn  41631  dihopelvalcpre  41685  dihord4  41695  dihord  41701  dihmeetlem4preN  41743  dih1dimatlem0  41765  dochsscl  41805  dochoccl  41806  dochord  41807  dochsat  41820  dochshpncl  41821  dochsatshpb  41889  dochshpsat  41891  mapdval4N  42069  mapdsn  42078  hdmap14lem12  42316  hdmapip0  42352  hlhillcs  42395  resuppsinopn  42794  mulgt0b2d  42922  mullt0b1d  42927  mullt0b2d  42928  riccrng  42966  ricdrng  42973  prjspner1  43058  mrefg2  43138  mzpmfp  43178  lzenom  43201  elpell14qr2  43293  elpell1qr2  43303  pellfund14b  43330  congabseq  43405  acongeq  43414  jm2.23  43427  jm2.20nn  43428  jm2.25lem1  43429  wepwsolem  43473  islssfg2  43502  lnmlmic  43519  dfacbasgrp  43539  unielss  43649  rfovcnvf1od  44434  dssmapnvod  44450  ntrclscls00  44496  rfcnpre3  45467  rfcnpre4  45468  ssmapsn  45648  rnmptssbi  45692  infxrgelbrnmpt  45886  xnegre  45898  xrpnf  45917  rexanuz2nf  45924  ioossioobi  45951  iccshift  45952  iocopn  45954  eliccelioc  45955  iooshift  45956  icoopn  45959  qinioo  45969  limcdm0  46052  islptre  46053  islpcn  46071  limcresioolb  46075  climuzlem  46175  climlimsup  46192  liminfgelimsup  46214  liminfgelimsupuz  46220  climliminf  46238  climliminflimsup  46240  climliminflimsup2  46241  xlimpnfxnegmnf  46246  xlimbr  46259  xlimmnfv  46266  xlimpnfv  46270  xlimclim2  46272  dfxlim2v  46279  climresdm  46282  xlimresdm  46291  xlimliminflimsup  46294  fperdvper  46351  itgperiod  46413  fourierdlem32  46571  fourierdlem33  46572  fourierdlem48  46586  fourierdlem49  46587  fourierdlem71  46609  fourierdlem81  46619  preimagelt  47131  preimalegt  47132  smfliminflem  47262  smfliminfmpt  47264  chnsubseqwl  47311  fcoresfob  47506  m1mod0mod1  47788  uhgrimedg  48325  isubgr3stgrlem8  48407  rngcinvALTV  48710  ringcinvALTV  48744  xpco2  49290  fvconstr  49295  fvconstrn0  49296  lubeldm2  49389  glbeldm2  49390  upeu2lem  49461  sectpropd  49470  invpropd  49472  isopropd  49474  cicerALT  49479  cicpropd  49483  up1st2ndb  49620  uobffth  49651  uobeqw  49652  natoppfb  49664  oppc1stflem  49720  fucofulem1  49743  functhinclem1  49877  fullthinc  49883  thincciso4  49890  thinciso  49903  functermclem  49940  termcterm3  49948  termcciso  49949  termcarweu  49961  termfucterm  49977  prstchom2ALT  49997  lanval2  50060  ranval2  50063