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  4791  frsn  5719  funfvbrb  7005  iinpreima  7023  fcdmssb  7076  fnprb  7164  fntpb  7165  fpr2g  7167  nvocnv  7238  fsnex  7240  f1ocnv2d  7622  resf1extb  7890  el2xptp0  7994  1stconst  8056  2ndconst  8057  cnvf1o  8067  fimaproj  8091  tfrlem15  8337  oeeui  8543  ersymb  8662  swoer  8679  erth  8702  boxriin  8890  boxcutc  8891  domunsncan  9018  pw2f1olem  9022  enen1  9058  enen2  9059  domen1  9060  domen2  9061  sdomen1  9062  sdomen2  9063  xpmapenlem  9085  ensymfib  9125  ordiso2  9444  wdomen1  9505  wdomen2  9506  fin23lem26  10254  fpwwe2lem7  10566  r1wunlim  10666  mul2lt0bi  13035  ixxun  13298  xov1plusxeqvd  13435  fzsplit2  13486  fseq1p1m1  13535  elfz2nn0  13555  flflp1  13745  modaddb  13847  modsubdir  13881  zesq  14167  expnngt1b  14183  hashprg  14336  hashgt0elexb  14343  hashbclem  14393  hashge2el2difb  14423  rereb  15062  rlimclim  15488  iserex  15599  caucvgb  15622  mptfzshft  15720  fsumrev  15721  climcnds  15793  fprodrev  15919  dvdsadd2b  16252  nn0ob  16330  bitsfzo  16381  dfgcd2  16492  dvdsmulgcd  16502  lcmgcdeq  16558  qden1elz  16703  mrcidb  17552  mrieqvlemd  17566  isacs2  17590  cicer  17744  ssclem  17757  issubc3  17787  ffthiso  17869  fuciso  17916  setcmon  18025  setcepi  18026  setcinv  18028  catciso  18049  acsfiindd  18488  issstrmgm  18556  mgmhmf1o  18603  issubmgm2  18606  subsubmgm  18613  resmgmhm2b  18616  issubmnd  18664  mhmf1o  18699  subsubm  18719  resmhm2b  18725  grpinvid1  18899  grpinvid2  18900  subsubg  19057  ssnmz  19074  ghmf1  19154  kerf1ghm  19155  ghmf1o  19156  conjnmzb  19161  subggim  19174  gicsubgen  19187  ghmqusnsglem1  19188  ghmquskerlem1  19191  ghmqusker  19195  gass  19209  odf1  19468  gex1  19497  fislw  19531  sylow3lem2  19534  sylow3lem6  19538  lsmdisj2a  19593  lsmdisj2b  19594  efgred2  19659  dmdprdsplit  19955  2nsgsimpgd  20010  simpgnsgbid  20011  ablsimpgd  20024  0unit  20281  irrednegb  20316  rnghmf1o  20337  rhmf1o  20376  subsubrng  20448  subrgunit  20475  subsubrg  20483  rngcinv  20522  ringcinv  20556  isdrng2  20628  issubdrg  20665  islss3  20841  islss4  20844  ellspsn6  20876  lspsneq0b  20895  islmhm2  20921  lmhmf1o  20929  reslmhm2b  20937  lssvs0or  20996  lvecinv  20999  ellspsn4  21010  lspdisjb  21012  islbs2  21040  islbs3  21041  dflidl2rng  21104  rngringbd  21194  prmirredlem  21358  islindf3  21711  lindsmm  21713  lsslindf  21715  lsslinds  21716  issubassa  21752  sraassab  21753  issubassa2  21777  gsumbagdiag  21816  subrgasclcl  21950  ply1scleq  22168  matunit  22541  slesolinvbi  22544  en2top  22848  elcls  22936  neindisj2  22986  neiptopnei  22995  neiptopreu  22996  maxlp  23010  neitr  23043  iscncl  23132  cncnp  23143  isreg2  23240  dis2ndc  23323  1stccnp  23325  islly2  23347  dislly  23360  dissnlocfin  23392  kgencmp2  23409  pt1hmeo  23669  xkocnv  23677  t0kq  23681  uffixfr  23786  flimcf  23845  cnpflf2  23863  fclscf  23888  cnextf  23929  utopsnneiplem  24111  isucn2  24142  cfilucfil  24423  psmetutop  24431  restmetu  24434  tngngp2  24516  tngngp  24518  nmoleub  24595  metdseq0  24719  cnheibor  24830  pcophtb  24905  nmoleub2lem  24990  lmmbr  25134  iscfil3  25149  cmetss  25192  cldcss  25317  mbfeqalem2  25519  mbfposb  25530  itg2const2  25618  itgss3  25692  plyco0  26073  dgrlt  26148  ulm2  26270  coseq00topi  26387  coseq0negpitopi  26388  sineq0  26409  relogbcxpb  26673  atans2  26817  xrlimcnp  26854  dchrelbas2  27124  dchrn0  27137  2sqb  27319  nosupbnd2  27604  noinfbnd2  27619  slerec  27707  sltmul2  28050  istrkg2ld  28363  tgcgreqb  28384  tgbtwncomb  28392  trgcgrg  28418  legov  28488  legov2  28489  legov3  28501  hlbtwn  28514  tglineelsb2  28535  tglinecom  28538  colline  28552  mirinv  28569  mirbtwnb  28575  mirbtwnhl  28583  perpcom  28616  isperp2  28618  oppcom  28647  opphllem3  28652  lnopp2hpgb  28666  colopp  28672  colhp  28673  lmieu  28687  iscgra1  28713  dfcgra2  28733  edgnbusgreu  29270  nb3grprlem1  29283  lfgriswlk  29590  eleclclwwlknlem2  29963  clwwlknscsh  29964  clwwlknon1  29999  numclwwlk2lem1  30278  grpoinvid1  30430  grpoinvid2  30431  leopmul  32036  hst1h  32129  eqelbid  32377  diffib  32423  ifnebib  32451  iinabrex  32471  disjabrex  32484  disjabrexf  32485  erbr3b  32518  f1o3d  32524  funimass4f  32534  2ndimaxp  32543  fgreu  32569  fcnvgreu  32570  1stpreimas  32602  fcobij  32618  resf1o  32626  nn0xmulclb  32667  fzsplit3  32689  fzo0opth  32701  sgn3da  32732  sgnnbi  32736  sgnpbi  32737  sgnmulsgn  32740  sgnmulsgp  32741  eliccioo  32824  mgcmntco  32893  dfmgc2lem  32894  dfmgc2  32895  pwrssmgc  32899  mgcf1o  32902  mndlrinvb  32939  mndlactfo  32941  mndractfo  32943  mndlactf1o  32944  mndractf1o  32945  gsumhashmul  32974  gsumwrd2dccatlem  32979  ogrpinv0le  33002  ogrpaddltbi  33005  ogrpaddltrbid  33007  ogrpinv0lt  33009  cyc3genpm  33082  isarchi3  33114  prmsimpcyc  33154  elrgspnsubrunlem1  33171  elrgspnsubrun  33173  domnlcanbOLD  33204  isdrng4  33218  fracerl  33229  qsxpid  33306  dvdsruasso  33329  dvdsruasso2  33330  dvdsrspss  33331  grplsmid  33348  quslsm  33349  nsgmgc  33356  nsgqusf1olem2  33358  nsgqusf1olem3  33359  pidlnzb  33366  unitpidl1  33368  elrspunidl  33372  elrspunsn  33373  drngidl  33377  drngidlhash  33378  isprmidlc  33391  prmidl0  33394  qsidom  33398  mxidlirred  33416  mxidlnzrb  33424  qsdrng  33441  rsprprmprmidlb  33467  rprmirredb  33476  deg1le0eq0  33515  ply1unit  33517  lvecdim0  33575  extdg1b  33635  fldextrspunlsp  33642  irngnzply1  33659  1smat1  33767  ist0cld  33796  qtophaus  33799  reff  33802  locfinreflem  33803  cmpcref  33813  zarcls1  33832  zarclsun  33833  zarclsiin  33834  zarclssn  33836  metider  33857  pstmfval  33859  qqhval2  33945  aean  34207  imambfm  34226  eulerpartlemgvv  34340  orvcgteel  34432  orvclteel  34437  ballotlemsf1o  34478  actfunsnf1o  34568  reprsuc  34579  reprpmtf1o  34590  sconnpi1  35199  brofs2  36038  brifs2  36039  broutsideof2  36083  bj-abv  36867  irrdiff  37287  ltflcei  37575  poimirlem25  37612  ismblfin  37628  cnambfre  37635  ftc1anclem6  37665  ismndo1  37840  isdrngo2  37925  eqvrelsymb  38570  eqvrelth  38575  lshpnelb  38950  lshpnel2N  38951  lsatspn0  38966  lsatelbN  38972  lsat0cv  38999  lcvexch  39005  lcv1  39007  lkrshp3  39072  lkrpssN  39129  lkrss2N  39135  cvlsupr2  39309  atcvrlln  39487  llncvrlpln  39525  2llnmj  39527  lplncvrlvol  39583  2lplnmj  39589  polcon2bN  39887  pcl0bN  39890  lhpmcvr3  39992  lhpmatb  39998  ltrncoidN  40095  ltrneq3  40175  ltrniotavalbN  40551  cdlemg1cN  40554  diclspsn  41161  dihopelvalcpre  41215  dihord4  41225  dihord  41231  dihmeetlem4preN  41273  dih1dimatlem0  41295  dochsscl  41335  dochoccl  41336  dochord  41337  dochsat  41350  dochshpncl  41351  dochsatshpb  41419  dochshpsat  41421  mapdval4N  41599  mapdsn  41608  hdmap14lem12  41846  hdmapip0  41882  hlhillcs  41925  resuppsinopn  42324  mulgt0b2d  42439  mullt0b1d  42444  mullt0b2d  42445  riccrng  42483  ricdrng  42490  prjspner1  42587  mrefg2  42668  mzpmfp  42708  lzenom  42731  elpell14qr2  42823  elpell1qr2  42833  pellfund14b  42860  congabseq  42936  acongeq  42945  jm2.23  42958  jm2.20nn  42959  jm2.25lem1  42960  wepwsolem  43004  islssfg2  43033  lnmlmic  43050  dfacbasgrp  43070  unielss  43180  rfovcnvf1od  43966  dssmapnvod  43982  ntrclscls00  44028  rfcnpre3  45000  rfcnpre4  45001  ssmapsn  45183  rnmptssbi  45227  infxrgelbrnmpt  45423  xnegre  45435  xrpnf  45454  rexanuz2nf  45461  ioossioobi  45488  iccshift  45489  iocopn  45491  eliccelioc  45492  iooshift  45493  icoopn  45496  qinioo  45506  limcdm0  45589  islptre  45590  islpcn  45610  limcresioolb  45614  climuzlem  45714  climlimsup  45731  liminfgelimsup  45753  liminfgelimsupuz  45759  climliminf  45777  climliminflimsup  45779  climliminflimsup2  45780  xlimpnfxnegmnf  45785  xlimbr  45798  xlimmnfv  45805  xlimpnfv  45809  xlimclim2  45811  dfxlim2v  45818  climresdm  45821  xlimresdm  45830  xlimliminflimsup  45833  fperdvper  45890  itgperiod  45952  fourierdlem32  46110  fourierdlem33  46111  fourierdlem48  46125  fourierdlem49  46126  fourierdlem71  46148  fourierdlem81  46158  preimagelt  46670  preimalegt  46671  smfliminflem  46801  smfliminfmpt  46803  fcoresfob  47046  m1mod0mod1  47328  uhgrimedg  47864  isubgr3stgrlem8  47945  rngcinvALTV  48237  ringcinvALTV  48271  xpco2  48818  fvconstr  48823  fvconstrn0  48824  lubeldm2  48917  glbeldm2  48918  upeu2lem  48990  sectpropd  48999  invpropd  49001  isopropd  49003  cicerALT  49008  cicpropd  49012  up1st2ndb  49149  uobffth  49180  uobeqw  49181  natoppfb  49193  oppc1stflem  49249  fucofulem1  49272  functhinclem1  49406  fullthinc  49412  thincciso4  49419  thinciso  49432  functermclem  49469  termcterm3  49477  termcciso  49478  termcarweu  49490  termfucterm  49506  prstchom2ALT  49526  lanval2  49589  ranval2  49592