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  4774  frsn  5719  funfvbrb  7003  iinpreima  7021  fcdmssb  7074  fnprb  7163  fntpb  7164  fpr2g  7166  nvocnv  7236  fsnex  7238  f1ocnv2d  7620  resf1extb  7885  el2xptp0  7989  1stconst  8050  2ndconst  8051  cnvf1o  8061  fimaproj  8085  tfrlem15  8331  oeeui  8538  ersymb  8658  swoer  8675  erth  8698  boxriin  8888  boxcutc  8889  domunsncan  9015  pw2f1olem  9019  enen1  9055  enen2  9056  domen1  9057  domen2  9058  sdomen1  9059  sdomen2  9060  xpmapenlem  9082  ensymfib  9118  ordiso2  9430  wdomen1  9491  wdomen2  9492  fin23lem26  10247  fpwwe2lem7  10560  r1wunlim  10660  mul2lt0bi  13050  ixxun  13314  xov1plusxeqvd  13451  fzsplit2  13503  fseq1p1m1  13552  elfz2nn0  13572  flflp1  13766  modaddb  13868  modsubdir  13902  zesq  14188  expnngt1b  14204  hashprg  14357  hashgt0elexb  14364  hashbclem  14414  hashge2el2difb  14444  rereb  15082  rlimclim  15508  iserex  15619  caucvgb  15642  mptfzshft  15740  fsumrev  15741  climcnds  15816  fprodrev  15942  dvdsadd2b  16275  nn0ob  16353  bitsfzo  16404  dfgcd2  16515  dvdsmulgcd  16525  lcmgcdeq  16581  qden1elz  16727  mrcidb  17581  mrieqvlemd  17595  isacs2  17619  cicer  17773  ssclem  17786  issubc3  17816  ffthiso  17898  fuciso  17945  setcmon  18054  setcepi  18055  setcinv  18057  catciso  18078  acsfiindd  18519  issstrmgm  18621  mgmhmf1o  18668  issubmgm2  18671  subsubmgm  18678  resmgmhm2b  18681  issubmnd  18729  mhmf1o  18764  subsubm  18784  resmhm2b  18790  grpinvid1  18967  grpinvid2  18968  subsubg  19125  ssnmz  19141  ghmf1  19221  kerf1ghm  19222  ghmf1o  19223  conjnmzb  19228  subggim  19241  gicsubgen  19254  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmqusker  19262  gass  19276  odf1  19537  gex1  19566  fislw  19600  sylow3lem2  19603  sylow3lem6  19607  lsmdisj2a  19662  lsmdisj2b  19663  efgred2  19728  dmdprdsplit  20024  2nsgsimpgd  20079  simpgnsgbid  20080  ablsimpgd  20093  ogrpinv0le  20111  ogrpaddltbi  20114  ogrpaddltrbid  20116  ogrpinv0lt  20118  0unit  20376  irrednegb  20411  rnghmf1o  20432  rhmf1o  20470  subsubrng  20540  subrgunit  20567  subsubrg  20575  rngcinv  20614  ringcinv  20648  isdrng2  20720  issubdrg  20757  islss3  20954  islss4  20957  ellspsn6  20989  lspsneq0b  21008  islmhm2  21033  lmhmf1o  21041  reslmhm2b  21049  lssvs0or  21108  lvecinv  21111  ellspsn4  21122  lspdisjb  21124  islbs2  21152  islbs3  21153  dflidl2rng  21216  rngringbd  21306  prmirredlem  21452  islindf3  21806  lindsmm  21808  lsslindf  21810  lsslinds  21811  issubassa  21847  sraassab  21848  issubassa2  21872  gsumbagdiag  21911  subrgasclcl  22045  ply1scleq  22270  matunit  22643  slesolinvbi  22646  en2top  22950  elcls  23038  neindisj2  23088  neiptopnei  23097  neiptopreu  23098  maxlp  23112  neitr  23145  iscncl  23234  cncnp  23245  isreg2  23342  dis2ndc  23425  1stccnp  23427  islly2  23449  dislly  23462  dissnlocfin  23494  kgencmp2  23511  pt1hmeo  23771  xkocnv  23779  t0kq  23783  uffixfr  23888  flimcf  23947  cnpflf2  23965  fclscf  23990  cnextf  24031  utopsnneiplem  24212  isucn2  24243  cfilucfil  24524  psmetutop  24532  restmetu  24535  tngngp2  24617  tngngp  24619  nmoleub  24696  metdseq0  24820  cnheibor  24922  pcophtb  24996  nmoleub2lem  25081  lmmbr  25225  iscfil3  25240  cmetss  25283  cldcss  25408  mbfeqalem2  25609  mbfposb  25620  itg2const2  25708  itgss3  25782  plyco0  26157  dgrlt  26231  ulm2  26350  coseq00topi  26466  coseq0negpitopi  26467  sineq0  26488  relogbcxpb  26751  atans2  26895  xrlimcnp  26932  dchrelbas2  27200  dchrn0  27213  2sqb  27395  nosupbnd2  27680  noinfbnd2  27695  lesrec  27791  ltmuls2  28163  elreno2  28487  istrkg2ld  28528  tgcgreqb  28549  tgbtwncomb  28557  trgcgrg  28583  legov  28653  legov2  28654  legov3  28666  hlbtwn  28679  tglineelsb2  28700  tglinecom  28703  colline  28717  mirinv  28734  mirbtwnb  28740  mirbtwnhl  28748  perpcom  28781  isperp2  28783  oppcom  28812  opphllem3  28817  lnopp2hpgb  28831  colopp  28837  colhp  28838  lmieu  28852  iscgra1  28878  dfcgra2  28898  edgnbusgreu  29436  nb3grprlem1  29449  lfgriswlk  29755  eleclclwwlknlem2  30131  clwwlknscsh  30132  clwwlknon1  30167  numclwwlk2lem1  30446  grpoinvid1  30599  grpoinvid2  30600  leopmul  32205  hst1h  32298  eqelbid  32544  diffib  32591  ifnebib  32619  iinabrex  32639  disjabrex  32652  disjabrexf  32653  erbr3b  32690  f1o3d  32699  funimass4f  32710  2ndimaxp  32719  fgreu  32744  fcnvgreu  32745  1stpreimas  32779  fcobij  32793  cocnvf1o  32802  resf1o  32803  nn0xmulclb  32844  fzsplit3  32866  fzo0opth  32876  sgn3da  32907  sgnnbi  32911  sgnpbi  32912  sgnmulsgn  32915  sgnmulsgp  32916  eliccioo  32990  mgcmntco  33054  dfmgc2lem  33055  dfmgc2  33056  pwrssmgc  33060  mgcf1o  33063  mndlrinvb  33085  mndlactfo  33087  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  gsumhashmul  33128  gsumwrd2dccatlem  33138  cyc3genpm  33213  isarchi3  33248  prmsimpcyc  33289  elrgspnsubrunlem1  33308  elrgspnsubrun  33310  domnlcanbOLD  33342  isdrng4  33356  fracerl  33367  qsxpid  33422  dvdsruasso  33445  dvdsruasso2  33446  dvdsrspss  33447  grplsmid  33464  quslsm  33465  nsgmgc  33472  nsgqusf1olem2  33474  nsgqusf1olem3  33475  pidlnzb  33482  unitpidl1  33484  elrspunidl  33488  elrspunsn  33489  drngidl  33493  drngidlhash  33494  isprmidlc  33507  prmidl0  33510  qsidom  33514  mxidlirred  33532  mxidlnzrb  33540  qsdrng  33557  rsprprmprmidlb  33583  rprmirredb  33592  deg1le0eq0  33633  ply1unit  33635  evlextv  33686  mplvrpmrhm  33691  esplyfv1  33713  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  lvecdim0  33751  extdg1b  33811  fldextrspunlsp  33818  irngnzply1  33835  1smat1  33948  ist0cld  33977  qtophaus  33980  reff  33983  locfinreflem  33984  cmpcref  33994  zarcls1  34013  zarclsun  34014  zarclsiin  34015  zarclssn  34017  metider  34038  pstmfval  34040  qqhval2  34126  aean  34388  imambfm  34406  eulerpartlemgvv  34520  orvcgteel  34612  orvclteel  34617  ballotlemsf1o  34658  actfunsnf1o  34748  reprsuc  34759  reprpmtf1o  34770  sconnpi1  35421  brofs2  36259  brifs2  36260  broutsideof2  36304  ttc0elw  36709  bj-abv  37213  irrdiff  37640  ltflcei  37929  poimirlem25  37966  ismblfin  37982  cnambfre  37989  ftc1anclem6  38019  ismndo1  38194  isdrngo2  38279  eqvrelsymb  39011  eqvrelth  39016  lshpnelb  39430  lshpnel2N  39431  lsatspn0  39446  lsatelbN  39452  lsat0cv  39479  lcvexch  39485  lcv1  39487  lkrshp3  39552  lkrpssN  39609  lkrss2N  39615  cvlsupr2  39789  atcvrlln  39966  llncvrlpln  40004  2llnmj  40006  lplncvrlvol  40062  2lplnmj  40068  polcon2bN  40366  pcl0bN  40369  lhpmcvr3  40471  lhpmatb  40477  ltrncoidN  40574  ltrneq3  40654  ltrniotavalbN  41030  cdlemg1cN  41033  diclspsn  41640  dihopelvalcpre  41694  dihord4  41704  dihord  41710  dihmeetlem4preN  41752  dih1dimatlem0  41774  dochsscl  41814  dochoccl  41815  dochord  41816  dochsat  41829  dochshpncl  41830  dochsatshpb  41898  dochshpsat  41900  mapdval4N  42078  mapdsn  42087  hdmap14lem12  42325  hdmapip0  42361  hlhillcs  42404  resuppsinopn  42795  mulgt0b2d  42923  mullt0b1d  42928  mullt0b2d  42929  riccrng  42967  ricdrng  42974  prjspner1  43059  mrefg2  43139  mzpmfp  43179  lzenom  43202  elpell14qr2  43290  elpell1qr2  43300  pellfund14b  43327  congabseq  43402  acongeq  43411  jm2.23  43424  jm2.20nn  43425  jm2.25lem1  43426  wepwsolem  43470  islssfg2  43499  lnmlmic  43516  dfacbasgrp  43536  unielss  43646  rfovcnvf1od  44431  dssmapnvod  44447  ntrclscls00  44493  rfcnpre3  45464  rfcnpre4  45465  ssmapsn  45645  rnmptssbi  45689  infxrgelbrnmpt  45882  xnegre  45894  xrpnf  45913  rexanuz2nf  45920  ioossioobi  45947  iccshift  45948  iocopn  45950  eliccelioc  45951  iooshift  45952  icoopn  45955  qinioo  45965  limcdm0  46048  islptre  46049  islpcn  46067  limcresioolb  46071  climuzlem  46171  climlimsup  46188  liminfgelimsup  46210  liminfgelimsupuz  46216  climliminf  46234  climliminflimsup  46236  climliminflimsup2  46237  xlimpnfxnegmnf  46242  xlimbr  46255  xlimmnfv  46262  xlimpnfv  46266  xlimclim2  46268  dfxlim2v  46275  climresdm  46278  xlimresdm  46287  xlimliminflimsup  46290  fperdvper  46347  itgperiod  46409  fourierdlem32  46567  fourierdlem33  46568  fourierdlem48  46582  fourierdlem49  46583  fourierdlem71  46605  fourierdlem81  46615  preimagelt  47127  preimalegt  47128  smfliminflem  47258  smfliminfmpt  47260  chnsubseqwl  47309  fcoresfob  47520  m1mod0mod1  47808  uhgrimedg  48367  isubgr3stgrlem8  48449  rngcinvALTV  48752  ringcinvALTV  48786  xpco2  49332  fvconstr  49337  fvconstrn0  49338  lubeldm2  49431  glbeldm2  49432  upeu2lem  49503  sectpropd  49512  invpropd  49514  isopropd  49516  cicerALT  49521  cicpropd  49525  up1st2ndb  49662  uobffth  49693  uobeqw  49694  natoppfb  49706  oppc1stflem  49762  fucofulem1  49785  functhinclem1  49919  fullthinc  49925  thincciso4  49932  thinciso  49945  functermclem  49982  termcterm3  49990  termcciso  49991  termcarweu  50003  termfucterm  50019  prstchom2ALT  50039  lanval2  50102  ranval2  50105