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  eqsndOLD  4775  frsn  5713  funfvbrb  6998  iinpreima  7016  fcdmssb  7069  fnprb  7157  fntpb  7158  fpr2g  7160  nvocnv  7230  fsnex  7232  f1ocnv2d  7614  resf1extb  7879  el2xptp0  7983  1stconst  8044  2ndconst  8045  cnvf1o  8055  fimaproj  8079  tfrlem15  8325  oeeui  8532  ersymb  8652  swoer  8669  erth  8692  boxriin  8882  boxcutc  8883  domunsncan  9009  pw2f1olem  9013  enen1  9049  enen2  9050  domen1  9051  domen2  9052  sdomen1  9053  sdomen2  9054  xpmapenlem  9076  ensymfib  9112  ordiso2  9424  wdomen1  9485  wdomen2  9486  fin23lem26  10241  fpwwe2lem7  10554  r1wunlim  10654  mul2lt0bi  13044  ixxun  13308  xov1plusxeqvd  13445  fzsplit2  13497  fseq1p1m1  13546  elfz2nn0  13566  flflp1  13760  modaddb  13862  modsubdir  13896  zesq  14182  expnngt1b  14198  hashprg  14351  hashgt0elexb  14358  hashbclem  14408  hashge2el2difb  14438  rereb  15076  rlimclim  15502  iserex  15613  caucvgb  15636  mptfzshft  15734  fsumrev  15735  climcnds  15810  fprodrev  15936  dvdsadd2b  16269  nn0ob  16347  bitsfzo  16398  dfgcd2  16509  dvdsmulgcd  16519  lcmgcdeq  16575  qden1elz  16721  mrcidb  17575  mrieqvlemd  17589  isacs2  17613  cicer  17767  ssclem  17780  issubc3  17810  ffthiso  17892  fuciso  17939  setcmon  18048  setcepi  18049  setcinv  18051  catciso  18072  acsfiindd  18513  issstrmgm  18615  mgmhmf1o  18662  issubmgm2  18665  subsubmgm  18672  resmgmhm2b  18675  issubmnd  18723  mhmf1o  18758  subsubm  18778  resmhm2b  18784  grpinvid1  18961  grpinvid2  18962  subsubg  19119  ssnmz  19135  ghmf1  19215  kerf1ghm  19216  ghmf1o  19217  conjnmzb  19222  subggim  19235  gicsubgen  19248  ghmqusnsglem1  19249  ghmquskerlem1  19252  ghmqusker  19256  gass  19270  odf1  19531  gex1  19560  fislw  19594  sylow3lem2  19597  sylow3lem6  19601  lsmdisj2a  19656  lsmdisj2b  19657  efgred2  19722  dmdprdsplit  20018  2nsgsimpgd  20073  simpgnsgbid  20074  ablsimpgd  20087  ogrpinv0le  20105  ogrpaddltbi  20108  ogrpaddltrbid  20110  ogrpinv0lt  20112  0unit  20370  irrednegb  20405  rnghmf1o  20426  rhmf1o  20464  subsubrng  20534  subrgunit  20561  subsubrg  20569  rngcinv  20608  ringcinv  20642  isdrng2  20714  issubdrg  20751  islss3  20948  islss4  20951  ellspsn6  20983  lspsneq0b  21002  islmhm2  21028  lmhmf1o  21036  reslmhm2b  21044  lssvs0or  21103  lvecinv  21106  ellspsn4  21117  lspdisjb  21119  islbs2  21147  islbs3  21148  dflidl2rng  21211  rngringbd  21301  prmirredlem  21465  islindf3  21819  lindsmm  21821  lsslindf  21823  lsslinds  21824  issubassa  21860  sraassab  21861  issubassa2  21885  gsumbagdiag  21924  subrgasclcl  22058  ply1scleq  22283  matunit  22656  slesolinvbi  22659  en2top  22963  elcls  23051  neindisj2  23101  neiptopnei  23110  neiptopreu  23111  maxlp  23125  neitr  23158  iscncl  23247  cncnp  23258  isreg2  23355  dis2ndc  23438  1stccnp  23440  islly2  23462  dislly  23475  dissnlocfin  23507  kgencmp2  23524  pt1hmeo  23784  xkocnv  23792  t0kq  23796  uffixfr  23901  flimcf  23960  cnpflf2  23978  fclscf  24003  cnextf  24044  utopsnneiplem  24225  isucn2  24256  cfilucfil  24537  psmetutop  24545  restmetu  24548  tngngp2  24630  tngngp  24632  nmoleub  24709  metdseq0  24833  cnheibor  24935  pcophtb  25009  nmoleub2lem  25094  lmmbr  25238  iscfil3  25253  cmetss  25296  cldcss  25421  mbfeqalem2  25622  mbfposb  25633  itg2const2  25721  itgss3  25795  plyco0  26170  dgrlt  26244  ulm2  26366  coseq00topi  26482  coseq0negpitopi  26483  sineq0  26504  relogbcxpb  26767  atans2  26911  xrlimcnp  26948  dchrelbas2  27217  dchrn0  27230  2sqb  27412  nosupbnd2  27697  noinfbnd2  27712  lesrec  27808  ltmuls2  28180  elreno2  28504  istrkg2ld  28545  tgcgreqb  28566  tgbtwncomb  28574  trgcgrg  28600  legov  28670  legov2  28671  legov3  28683  hlbtwn  28696  tglineelsb2  28717  tglinecom  28720  colline  28734  mirinv  28751  mirbtwnb  28757  mirbtwnhl  28765  perpcom  28798  isperp2  28800  oppcom  28829  opphllem3  28834  lnopp2hpgb  28848  colopp  28854  colhp  28855  lmieu  28869  iscgra1  28895  dfcgra2  28915  edgnbusgreu  29453  nb3grprlem1  29466  lfgriswlk  29773  eleclclwwlknlem2  30149  clwwlknscsh  30150  clwwlknon1  30185  numclwwlk2lem1  30464  grpoinvid1  30617  grpoinvid2  30618  leopmul  32223  hst1h  32316  eqelbid  32562  diffib  32609  ifnebib  32637  iinabrex  32657  disjabrex  32670  disjabrexf  32671  erbr3b  32708  f1o3d  32717  funimass4f  32728  2ndimaxp  32737  fgreu  32762  fcnvgreu  32763  1stpreimas  32797  fcobij  32811  cocnvf1o  32820  resf1o  32821  nn0xmulclb  32862  fzsplit3  32884  fzo0opth  32894  sgn3da  32925  sgnnbi  32929  sgnpbi  32930  sgnmulsgn  32933  sgnmulsgp  32934  eliccioo  33008  mgcmntco  33072  dfmgc2lem  33073  dfmgc2  33074  pwrssmgc  33078  mgcf1o  33081  mndlrinvb  33103  mndlactfo  33105  mndractfo  33107  mndlactf1o  33108  mndractf1o  33109  gsumhashmul  33146  gsumwrd2dccatlem  33156  cyc3genpm  33231  isarchi3  33266  prmsimpcyc  33307  elrgspnsubrunlem1  33326  elrgspnsubrun  33328  domnlcanbOLD  33360  isdrng4  33374  fracerl  33385  qsxpid  33440  dvdsruasso  33463  dvdsruasso2  33464  dvdsrspss  33465  grplsmid  33482  quslsm  33483  nsgmgc  33490  nsgqusf1olem2  33492  nsgqusf1olem3  33493  pidlnzb  33500  unitpidl1  33502  elrspunidl  33506  elrspunsn  33507  drngidl  33511  drngidlhash  33512  isprmidlc  33525  prmidl0  33528  qsidom  33532  mxidlirred  33550  mxidlnzrb  33558  qsdrng  33575  rsprprmprmidlb  33601  rprmirredb  33610  deg1le0eq0  33651  ply1unit  33653  evlextv  33704  mplvrpmrhm  33709  esplyfv1  33731  esplyfval1  33735  esplyfvaln  33736  esplyind  33737  lvecdim0  33769  extdg1b  33830  fldextrspunlsp  33837  irngnzply1  33854  1smat1  33967  ist0cld  33996  qtophaus  33999  reff  34002  locfinreflem  34003  cmpcref  34013  zarcls1  34032  zarclsun  34033  zarclsiin  34034  zarclssn  34036  metider  34057  pstmfval  34059  qqhval2  34145  aean  34407  imambfm  34425  eulerpartlemgvv  34539  orvcgteel  34631  orvclteel  34636  ballotlemsf1o  34677  actfunsnf1o  34767  reprsuc  34778  reprpmtf1o  34789  sconnpi1  35440  brofs2  36278  brifs2  36279  broutsideof2  36323  ttc0elw  36728  bj-abv  37232  irrdiff  37659  ltflcei  37946  poimirlem25  37983  ismblfin  37999  cnambfre  38006  ftc1anclem6  38036  ismndo1  38211  isdrngo2  38296  eqvrelsymb  39028  eqvrelth  39033  lshpnelb  39447  lshpnel2N  39448  lsatspn0  39463  lsatelbN  39469  lsat0cv  39496  lcvexch  39502  lcv1  39504  lkrshp3  39569  lkrpssN  39626  lkrss2N  39632  cvlsupr2  39806  atcvrlln  39983  llncvrlpln  40021  2llnmj  40023  lplncvrlvol  40079  2lplnmj  40085  polcon2bN  40383  pcl0bN  40386  lhpmcvr3  40488  lhpmatb  40494  ltrncoidN  40591  ltrneq3  40671  ltrniotavalbN  41047  cdlemg1cN  41050  diclspsn  41657  dihopelvalcpre  41711  dihord4  41721  dihord  41727  dihmeetlem4preN  41769  dih1dimatlem0  41791  dochsscl  41831  dochoccl  41832  dochord  41833  dochsat  41846  dochshpncl  41847  dochsatshpb  41915  dochshpsat  41917  mapdval4N  42095  mapdsn  42104  hdmap14lem12  42342  hdmapip0  42378  hlhillcs  42421  resuppsinopn  42812  mulgt0b2d  42940  mullt0b1d  42945  mullt0b2d  42946  riccrng  42984  ricdrng  42991  prjspner1  43076  mrefg2  43156  mzpmfp  43196  lzenom  43219  elpell14qr2  43311  elpell1qr2  43321  pellfund14b  43348  congabseq  43423  acongeq  43432  jm2.23  43445  jm2.20nn  43446  jm2.25lem1  43447  wepwsolem  43491  islssfg2  43520  lnmlmic  43537  dfacbasgrp  43557  unielss  43667  rfovcnvf1od  44452  dssmapnvod  44468  ntrclscls00  44514  rfcnpre3  45485  rfcnpre4  45486  ssmapsn  45666  rnmptssbi  45710  infxrgelbrnmpt  45903  xnegre  45915  xrpnf  45934  rexanuz2nf  45941  ioossioobi  45968  iccshift  45969  iocopn  45971  eliccelioc  45972  iooshift  45973  icoopn  45976  qinioo  45986  limcdm0  46069  islptre  46070  islpcn  46088  limcresioolb  46092  climuzlem  46192  climlimsup  46209  liminfgelimsup  46231  liminfgelimsupuz  46237  climliminf  46255  climliminflimsup  46257  climliminflimsup2  46258  xlimpnfxnegmnf  46263  xlimbr  46276  xlimmnfv  46283  xlimpnfv  46287  xlimclim2  46289  dfxlim2v  46296  climresdm  46299  xlimresdm  46308  xlimliminflimsup  46311  fperdvper  46368  itgperiod  46430  fourierdlem32  46588  fourierdlem33  46589  fourierdlem48  46603  fourierdlem49  46604  fourierdlem71  46626  fourierdlem81  46636  preimagelt  47148  preimalegt  47149  smfliminflem  47279  smfliminfmpt  47281  chnsubseqwl  47328  fcoresfob  47535  m1mod0mod1  47823  uhgrimedg  48382  isubgr3stgrlem8  48464  rngcinvALTV  48767  ringcinvALTV  48801  xpco2  49347  fvconstr  49352  fvconstrn0  49353  lubeldm2  49446  glbeldm2  49447  upeu2lem  49518  sectpropd  49527  invpropd  49529  isopropd  49531  cicerALT  49536  cicpropd  49540  up1st2ndb  49677  uobffth  49708  uobeqw  49709  natoppfb  49721  oppc1stflem  49777  fucofulem1  49800  functhinclem1  49934  fullthinc  49940  thincciso4  49947  thinciso  49960  functermclem  49997  termcterm3  50005  termcciso  50006  termcarweu  50018  termfucterm  50034  prstchom2ALT  50054  lanval2  50117  ranval2  50120