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  2733  eqsndOLD  4811  frsn  5753  funfvbrb  7051  iinpreima  7069  fcdmssb  7122  fnprb  7210  fntpb  7211  fpr2g  7213  nvocnv  7283  fsnex  7285  f1ocnv2d  7668  resf1extb  7938  el2xptp0  8043  1stconst  8107  2ndconst  8108  cnvf1o  8118  fimaproj  8142  tfrlem15  8414  oeeui  8622  ersymb  8741  swoer  8758  erth  8778  boxriin  8962  boxcutc  8963  domunsncan  9094  pw2f1olem  9098  enen1  9139  enen2  9140  domen1  9141  domen2  9142  sdomen1  9143  sdomen2  9144  xpmapenlem  9166  ensymfib  9206  ordiso2  9537  wdomen1  9598  wdomen2  9599  fin23lem26  10347  fpwwe2lem7  10659  r1wunlim  10759  mul2lt0bi  13123  ixxun  13385  xov1plusxeqvd  13520  fzsplit2  13571  fseq1p1m1  13620  elfz2nn0  13640  flflp1  13829  modsubdir  13963  zesq  14248  expnngt1b  14264  hashprg  14417  hashgt0elexb  14424  hashbclem  14474  hashge2el2difb  14504  rereb  15142  rlimclim  15565  iserex  15676  caucvgb  15699  mptfzshft  15797  fsumrev  15798  climcnds  15870  fprodrev  15996  dvdsadd2b  16326  nn0ob  16404  bitsfzo  16455  dfgcd2  16566  dvdsmulgcd  16576  lcmgcdeq  16632  qden1elz  16777  mrcidb  17630  mrieqvlemd  17644  isacs2  17668  cicer  17822  ssclem  17835  issubc3  17866  ffthiso  17948  fuciso  17995  setcmon  18104  setcepi  18105  setcinv  18107  catciso  18128  acsfiindd  18568  issstrmgm  18636  mgmhmf1o  18683  issubmgm2  18686  subsubmgm  18693  resmgmhm2b  18696  issubmnd  18744  mhmf1o  18779  subsubm  18799  resmhm2b  18805  grpinvid1  18979  grpinvid2  18980  subsubg  19137  ssnmz  19154  ghmf1  19234  kerf1ghm  19235  ghmf1o  19236  conjnmzb  19241  subggim  19254  gicsubgen  19267  ghmqusnsglem1  19268  ghmquskerlem1  19271  ghmqusker  19275  gass  19289  odf1  19549  gex1  19578  fislw  19612  sylow3lem2  19615  sylow3lem6  19619  lsmdisj2a  19674  lsmdisj2b  19675  efgred2  19740  dmdprdsplit  20036  2nsgsimpgd  20091  simpgnsgbid  20092  ablsimpgd  20105  0unit  20365  irrednegb  20400  rnghmf1o  20421  rhmf1o  20460  subsubrng  20532  subrgunit  20559  subsubrg  20567  rngcinv  20606  ringcinv  20640  isdrng2  20712  issubdrg  20750  islss3  20926  islss4  20929  ellspsn6  20961  lspsneq0b  20980  islmhm2  21006  lmhmf1o  21014  reslmhm2b  21022  lssvs0or  21081  lvecinv  21084  ellspsn4  21095  lspdisjb  21097  islbs2  21125  islbs3  21126  dflidl2rng  21191  rngringbd  21281  prmirredlem  21446  islindf3  21801  lindsmm  21803  lsslindf  21805  lsslinds  21806  issubassa  21842  sraassab  21843  issubassa2  21867  gsumbagdiag  21906  subrgasclcl  22040  ply1scleq  22258  matunit  22633  slesolinvbi  22636  en2top  22940  elcls  23028  neindisj2  23078  neiptopnei  23087  neiptopreu  23088  maxlp  23102  neitr  23135  iscncl  23224  cncnp  23235  isreg2  23332  dis2ndc  23415  1stccnp  23417  islly2  23439  dislly  23452  dissnlocfin  23484  kgencmp2  23501  pt1hmeo  23761  xkocnv  23769  t0kq  23773  uffixfr  23878  flimcf  23937  cnpflf2  23955  fclscf  23980  cnextf  24021  utopsnneiplem  24203  isucn2  24234  cfilucfil  24517  psmetutop  24525  restmetu  24528  tngngp2  24610  tngngp  24612  nmoleub  24689  metdseq0  24813  cnheibor  24924  pcophtb  24999  nmoleub2lem  25084  lmmbr  25229  iscfil3  25244  cmetss  25287  cldcss  25412  mbfeqalem2  25614  mbfposb  25625  itg2const2  25713  itgss3  25787  plyco0  26168  dgrlt  26243  ulm2  26365  coseq00topi  26481  coseq0negpitopi  26482  sineq0  26503  relogbcxpb  26767  atans2  26911  xrlimcnp  26948  dchrelbas2  27218  dchrn0  27231  2sqb  27413  nosupbnd2  27698  noinfbnd2  27713  slerec  27801  sltmul2  28134  istrkg2ld  28405  tgcgreqb  28426  tgbtwncomb  28434  trgcgrg  28460  legov  28530  legov2  28531  legov3  28543  hlbtwn  28556  tglineelsb2  28577  tglinecom  28580  colline  28594  mirinv  28611  mirbtwnb  28617  mirbtwnhl  28625  perpcom  28658  isperp2  28660  oppcom  28689  opphllem3  28694  lnopp2hpgb  28708  colopp  28714  colhp  28715  lmieu  28729  iscgra1  28755  dfcgra2  28775  edgnbusgreu  29313  nb3grprlem1  29326  lfgriswlk  29635  eleclclwwlknlem2  30009  clwwlknscsh  30010  clwwlknon1  30045  numclwwlk2lem1  30324  grpoinvid1  30476  grpoinvid2  30477  leopmul  32082  hst1h  32175  eqelbid  32423  diffib  32469  ifnebib  32498  iinabrex  32518  disjabrex  32531  disjabrexf  32532  erbr3b  32565  f1o3d  32573  funimass4f  32583  2ndimaxp  32592  fgreu  32618  fcnvgreu  32619  1stpreimas  32651  fcobij  32669  resf1o  32677  nn0xmulclb  32717  fzsplit3  32739  fzo0opth  32751  eliccioo  32858  mgcmntco  32928  dfmgc2lem  32929  dfmgc2  32930  pwrssmgc  32934  mgcf1o  32937  mndlrinvb  32974  mndlactfo  32976  mndractfo  32978  mndlactf1o  32979  mndractf1o  32980  gsumhashmul  33008  gsumwrd2dccatlem  33013  ogrpinv0le  33036  ogrpaddltbi  33039  ogrpaddltrbid  33041  ogrpinv0lt  33043  cyc3genpm  33116  isarchi3  33138  prmsimpcyc  33178  elrgspnsubrunlem1  33195  elrgspnsubrun  33197  domnlcanbOLD  33228  isdrng4  33242  fracerl  33253  qsxpid  33330  dvdsruasso  33353  dvdsruasso2  33354  dvdsrspss  33355  grplsmid  33372  quslsm  33373  nsgmgc  33380  nsgqusf1olem2  33382  nsgqusf1olem3  33383  pidlnzb  33390  unitpidl1  33392  elrspunidl  33396  elrspunsn  33397  drngidl  33401  drngidlhash  33402  isprmidlc  33415  prmidl0  33418  qsidom  33422  mxidlirred  33440  mxidlnzrb  33448  qsdrng  33465  rsprprmprmidlb  33491  rprmirredb  33500  deg1le0eq0  33538  ply1unit  33540  lvecdim0  33597  extdg1b  33659  fldextrspunlsp  33666  irngnzply1  33683  1smat1  33778  ist0cld  33807  qtophaus  33810  reff  33813  locfinreflem  33814  cmpcref  33824  zarcls1  33843  zarclsun  33844  zarclsiin  33845  zarclssn  33847  metider  33868  pstmfval  33870  qqhval2  33958  aean  34220  imambfm  34239  eulerpartlemgvv  34353  orvcgteel  34445  orvclteel  34450  ballotlemsf1o  34491  sgn3da  34519  sgnnbi  34523  sgnpbi  34524  sgnmulsgn  34527  sgnmulsgp  34528  actfunsnf1o  34594  reprsuc  34605  reprpmtf1o  34616  sconnpi1  35219  brofs2  36053  brifs2  36054  broutsideof2  36098  bj-abv  36882  irrdiff  37302  ltflcei  37590  poimirlem25  37627  ismblfin  37643  cnambfre  37650  ftc1anclem6  37680  ismndo1  37855  isdrngo2  37940  eqvrelsymb  38582  eqvrelth  38587  lshpnelb  38960  lshpnel2N  38961  lsatspn0  38976  lsatelbN  38982  lsat0cv  39009  lcvexch  39015  lcv1  39017  lkrshp3  39082  lkrpssN  39139  lkrss2N  39145  cvlsupr2  39319  atcvrlln  39497  llncvrlpln  39535  2llnmj  39537  lplncvrlvol  39593  2lplnmj  39599  polcon2bN  39897  pcl0bN  39900  lhpmcvr3  40002  lhpmatb  40008  ltrncoidN  40105  ltrneq3  40185  ltrniotavalbN  40561  cdlemg1cN  40564  diclspsn  41171  dihopelvalcpre  41225  dihord4  41235  dihord  41241  dihmeetlem4preN  41283  dih1dimatlem0  41305  dochsscl  41345  dochoccl  41346  dochord  41347  dochsat  41360  dochshpncl  41361  dochsatshpb  41429  dochshpsat  41431  mapdval4N  41609  mapdsn  41618  hdmap14lem12  41856  hdmapip0  41892  hlhillcs  41939  resuppsinopn  42372  riccrng  42511  ricdrng  42518  prjspner1  42615  mrefg2  42696  mzpmfp  42736  lzenom  42759  elpell14qr2  42851  elpell1qr2  42861  pellfund14b  42888  congabseq  42964  acongeq  42973  jm2.23  42986  jm2.20nn  42987  jm2.25lem1  42988  wepwsolem  43032  islssfg2  43061  lnmlmic  43078  dfacbasgrp  43098  unielss  43208  rfovcnvf1od  43994  dssmapnvod  44010  ntrclscls00  44056  rfcnpre3  45010  rfcnpre4  45011  ssmapsn  45193  rnmptssbi  45239  infxrgelbrnmpt  45437  xnegre  45449  xrpnf  45468  rexanuz2nf  45475  ioossioobi  45502  iccshift  45503  iocopn  45505  eliccelioc  45506  iooshift  45507  icoopn  45510  qinioo  45520  limcdm0  45605  islptre  45606  islpcn  45626  limcresioolb  45630  climuzlem  45730  climlimsup  45747  liminfgelimsup  45769  liminfgelimsupuz  45775  climliminf  45793  climliminflimsup  45795  climliminflimsup2  45796  xlimpnfxnegmnf  45801  xlimbr  45814  xlimmnfv  45821  xlimpnfv  45825  xlimclim2  45827  dfxlim2v  45834  climresdm  45837  xlimresdm  45846  xlimliminflimsup  45849  fperdvper  45906  itgperiod  45968  fourierdlem32  46126  fourierdlem33  46127  fourierdlem48  46141  fourierdlem49  46142  fourierdlem71  46164  fourierdlem81  46174  preimagelt  46686  preimalegt  46687  smfliminflem  46817  smfliminfmpt  46819  fcoresfob  47057  m1mod0mod1  47329  uspgrimprop  47846  isubgr3stgrlem8  47913  rngcinvALTV  48165  ringcinvALTV  48199  fvconstr  48746  fvconstrn0  48747  lubeldm2  48837  glbeldm2  48838  upeu2lem  48905  sectpropd  48911  invpropd  48913  isopropd  48915  cicerALT  48920  cicpropd  48924  up1st2ndb  48970  fucofulem1  49055  functhinclem1  49145  fullthinc  49151  thincciso4  49158  thinciso  49169  functermclem  49205  termcterm3  49213  termcciso  49214  termcarweu  49226  prstchom2ALT  49256