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  2728  eqsndOLD  4795  frsn  5726  funfvbrb  7023  iinpreima  7041  fcdmssb  7094  fnprb  7182  fntpb  7183  fpr2g  7185  nvocnv  7256  fsnex  7258  f1ocnv2d  7642  resf1extb  7910  el2xptp0  8015  1stconst  8079  2ndconst  8080  cnvf1o  8090  fimaproj  8114  tfrlem15  8360  oeeui  8566  ersymb  8685  swoer  8702  erth  8725  boxriin  8913  boxcutc  8914  domunsncan  9041  pw2f1olem  9045  enen1  9081  enen2  9082  domen1  9083  domen2  9084  sdomen1  9085  sdomen2  9086  xpmapenlem  9108  ensymfib  9148  ordiso2  9468  wdomen1  9529  wdomen2  9530  fin23lem26  10278  fpwwe2lem7  10590  r1wunlim  10690  mul2lt0bi  13059  ixxun  13322  xov1plusxeqvd  13459  fzsplit2  13510  fseq1p1m1  13559  elfz2nn0  13579  flflp1  13769  modaddb  13871  modsubdir  13905  zesq  14191  expnngt1b  14207  hashprg  14360  hashgt0elexb  14367  hashbclem  14417  hashge2el2difb  14447  rereb  15086  rlimclim  15512  iserex  15623  caucvgb  15646  mptfzshft  15744  fsumrev  15745  climcnds  15817  fprodrev  15943  dvdsadd2b  16276  nn0ob  16354  bitsfzo  16405  dfgcd2  16516  dvdsmulgcd  16526  lcmgcdeq  16582  qden1elz  16727  mrcidb  17576  mrieqvlemd  17590  isacs2  17614  cicer  17768  ssclem  17781  issubc3  17811  ffthiso  17893  fuciso  17940  setcmon  18049  setcepi  18050  setcinv  18052  catciso  18073  acsfiindd  18512  issstrmgm  18580  mgmhmf1o  18627  issubmgm2  18630  subsubmgm  18637  resmgmhm2b  18640  issubmnd  18688  mhmf1o  18723  subsubm  18743  resmhm2b  18749  grpinvid1  18923  grpinvid2  18924  subsubg  19081  ssnmz  19098  ghmf1  19178  kerf1ghm  19179  ghmf1o  19180  conjnmzb  19185  subggim  19198  gicsubgen  19211  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmqusker  19219  gass  19233  odf1  19492  gex1  19521  fislw  19555  sylow3lem2  19558  sylow3lem6  19562  lsmdisj2a  19617  lsmdisj2b  19618  efgred2  19683  dmdprdsplit  19979  2nsgsimpgd  20034  simpgnsgbid  20035  ablsimpgd  20048  0unit  20305  irrednegb  20340  rnghmf1o  20361  rhmf1o  20400  subsubrng  20472  subrgunit  20499  subsubrg  20507  rngcinv  20546  ringcinv  20580  isdrng2  20652  issubdrg  20689  islss3  20865  islss4  20868  ellspsn6  20900  lspsneq0b  20919  islmhm2  20945  lmhmf1o  20953  reslmhm2b  20961  lssvs0or  21020  lvecinv  21023  ellspsn4  21034  lspdisjb  21036  islbs2  21064  islbs3  21065  dflidl2rng  21128  rngringbd  21218  prmirredlem  21382  islindf3  21735  lindsmm  21737  lsslindf  21739  lsslinds  21740  issubassa  21776  sraassab  21777  issubassa2  21801  gsumbagdiag  21840  subrgasclcl  21974  ply1scleq  22192  matunit  22565  slesolinvbi  22568  en2top  22872  elcls  22960  neindisj2  23010  neiptopnei  23019  neiptopreu  23020  maxlp  23034  neitr  23067  iscncl  23156  cncnp  23167  isreg2  23264  dis2ndc  23347  1stccnp  23349  islly2  23371  dislly  23384  dissnlocfin  23416  kgencmp2  23433  pt1hmeo  23693  xkocnv  23701  t0kq  23705  uffixfr  23810  flimcf  23869  cnpflf2  23887  fclscf  23912  cnextf  23953  utopsnneiplem  24135  isucn2  24166  cfilucfil  24447  psmetutop  24455  restmetu  24458  tngngp2  24540  tngngp  24542  nmoleub  24619  metdseq0  24743  cnheibor  24854  pcophtb  24929  nmoleub2lem  25014  lmmbr  25158  iscfil3  25173  cmetss  25216  cldcss  25341  mbfeqalem2  25543  mbfposb  25554  itg2const2  25642  itgss3  25716  plyco0  26097  dgrlt  26172  ulm2  26294  coseq00topi  26411  coseq0negpitopi  26412  sineq0  26433  relogbcxpb  26697  atans2  26841  xrlimcnp  26878  dchrelbas2  27148  dchrn0  27161  2sqb  27343  nosupbnd2  27628  noinfbnd2  27643  slerec  27731  sltmul2  28074  istrkg2ld  28387  tgcgreqb  28408  tgbtwncomb  28416  trgcgrg  28442  legov  28512  legov2  28513  legov3  28525  hlbtwn  28538  tglineelsb2  28559  tglinecom  28562  colline  28576  mirinv  28593  mirbtwnb  28599  mirbtwnhl  28607  perpcom  28640  isperp2  28642  oppcom  28671  opphllem3  28676  lnopp2hpgb  28690  colopp  28696  colhp  28697  lmieu  28711  iscgra1  28737  dfcgra2  28757  edgnbusgreu  29294  nb3grprlem1  29307  lfgriswlk  29616  eleclclwwlknlem2  29990  clwwlknscsh  29991  clwwlknon1  30026  numclwwlk2lem1  30305  grpoinvid1  30457  grpoinvid2  30458  leopmul  32063  hst1h  32156  eqelbid  32404  diffib  32450  ifnebib  32478  iinabrex  32498  disjabrex  32511  disjabrexf  32512  erbr3b  32545  f1o3d  32551  funimass4f  32561  2ndimaxp  32570  fgreu  32596  fcnvgreu  32597  1stpreimas  32629  fcobij  32645  resf1o  32653  nn0xmulclb  32694  fzsplit3  32716  fzo0opth  32728  sgn3da  32759  sgnnbi  32763  sgnpbi  32764  sgnmulsgn  32767  sgnmulsgp  32768  eliccioo  32851  mgcmntco  32920  dfmgc2lem  32921  dfmgc2  32922  pwrssmgc  32926  mgcf1o  32929  mndlrinvb  32966  mndlactfo  32968  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsumhashmul  33001  gsumwrd2dccatlem  33006  ogrpinv0le  33029  ogrpaddltbi  33032  ogrpaddltrbid  33034  ogrpinv0lt  33036  cyc3genpm  33109  isarchi3  33141  prmsimpcyc  33181  elrgspnsubrunlem1  33198  elrgspnsubrun  33200  domnlcanbOLD  33231  isdrng4  33245  fracerl  33256  qsxpid  33333  dvdsruasso  33356  dvdsruasso2  33357  dvdsrspss  33358  grplsmid  33375  quslsm  33376  nsgmgc  33383  nsgqusf1olem2  33385  nsgqusf1olem3  33386  pidlnzb  33393  unitpidl1  33395  elrspunidl  33399  elrspunsn  33400  drngidl  33404  drngidlhash  33405  isprmidlc  33418  prmidl0  33421  qsidom  33425  mxidlirred  33443  mxidlnzrb  33451  qsdrng  33468  rsprprmprmidlb  33494  rprmirredb  33503  deg1le0eq0  33542  ply1unit  33544  lvecdim0  33602  extdg1b  33662  fldextrspunlsp  33669  irngnzply1  33686  1smat1  33794  ist0cld  33823  qtophaus  33826  reff  33829  locfinreflem  33830  cmpcref  33840  zarcls1  33859  zarclsun  33860  zarclsiin  33861  zarclssn  33863  metider  33884  pstmfval  33886  qqhval2  33972  aean  34234  imambfm  34253  eulerpartlemgvv  34367  orvcgteel  34459  orvclteel  34464  ballotlemsf1o  34505  actfunsnf1o  34595  reprsuc  34606  reprpmtf1o  34617  sconnpi1  35226  brofs2  36065  brifs2  36066  broutsideof2  36110  bj-abv  36894  irrdiff  37314  ltflcei  37602  poimirlem25  37639  ismblfin  37655  cnambfre  37662  ftc1anclem6  37692  ismndo1  37867  isdrngo2  37952  eqvrelsymb  38597  eqvrelth  38602  lshpnelb  38977  lshpnel2N  38978  lsatspn0  38993  lsatelbN  38999  lsat0cv  39026  lcvexch  39032  lcv1  39034  lkrshp3  39099  lkrpssN  39156  lkrss2N  39162  cvlsupr2  39336  atcvrlln  39514  llncvrlpln  39552  2llnmj  39554  lplncvrlvol  39610  2lplnmj  39616  polcon2bN  39914  pcl0bN  39917  lhpmcvr3  40019  lhpmatb  40025  ltrncoidN  40122  ltrneq3  40202  ltrniotavalbN  40578  cdlemg1cN  40581  diclspsn  41188  dihopelvalcpre  41242  dihord4  41252  dihord  41258  dihmeetlem4preN  41300  dih1dimatlem0  41322  dochsscl  41362  dochoccl  41363  dochord  41364  dochsat  41377  dochshpncl  41378  dochsatshpb  41446  dochshpsat  41448  mapdval4N  41626  mapdsn  41635  hdmap14lem12  41873  hdmapip0  41909  hlhillcs  41952  resuppsinopn  42351  mulgt0b2d  42466  mullt0b1d  42471  mullt0b2d  42472  riccrng  42510  ricdrng  42517  prjspner1  42614  mrefg2  42695  mzpmfp  42735  lzenom  42758  elpell14qr2  42850  elpell1qr2  42860  pellfund14b  42887  congabseq  42963  acongeq  42972  jm2.23  42985  jm2.20nn  42986  jm2.25lem1  42987  wepwsolem  43031  islssfg2  43060  lnmlmic  43077  dfacbasgrp  43097  unielss  43207  rfovcnvf1od  43993  dssmapnvod  44009  ntrclscls00  44055  rfcnpre3  45027  rfcnpre4  45028  ssmapsn  45210  rnmptssbi  45254  infxrgelbrnmpt  45450  xnegre  45462  xrpnf  45481  rexanuz2nf  45488  ioossioobi  45515  iccshift  45516  iocopn  45518  eliccelioc  45519  iooshift  45520  icoopn  45523  qinioo  45533  limcdm0  45616  islptre  45617  islpcn  45637  limcresioolb  45641  climuzlem  45741  climlimsup  45758  liminfgelimsup  45780  liminfgelimsupuz  45786  climliminf  45804  climliminflimsup  45806  climliminflimsup2  45807  xlimpnfxnegmnf  45812  xlimbr  45825  xlimmnfv  45832  xlimpnfv  45836  xlimclim2  45838  dfxlim2v  45845  climresdm  45848  xlimresdm  45857  xlimliminflimsup  45860  fperdvper  45917  itgperiod  45979  fourierdlem32  46137  fourierdlem33  46138  fourierdlem48  46152  fourierdlem49  46153  fourierdlem71  46175  fourierdlem81  46185  preimagelt  46697  preimalegt  46698  smfliminflem  46828  smfliminfmpt  46830  fcoresfob  47073  m1mod0mod1  47355  uhgrimedg  47891  isubgr3stgrlem8  47972  rngcinvALTV  48264  ringcinvALTV  48298  xpco2  48845  fvconstr  48850  fvconstrn0  48851  lubeldm2  48944  glbeldm2  48945  upeu2lem  49017  sectpropd  49026  invpropd  49028  isopropd  49030  cicerALT  49035  cicpropd  49039  up1st2ndb  49176  uobffth  49207  uobeqw  49208  natoppfb  49220  oppc1stflem  49276  fucofulem1  49299  functhinclem1  49433  fullthinc  49439  thincciso4  49446  thinciso  49459  functermclem  49496  termcterm3  49504  termcciso  49505  termcarweu  49517  termfucterm  49533  prstchom2ALT  49553  lanval2  49616  ranval2  49619