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  eqrdav  2739  eqsndOLD  4856  frsn  5787  funfvbrb  7084  iinpreima  7102  fcdmssb  7156  fnprb  7245  fntpb  7246  fpr2g  7248  nvocnv  7317  fsnex  7319  f1ocnv2d  7703  el2xptp0  8077  1stconst  8141  2ndconst  8142  cnvf1o  8152  fimaproj  8176  tfrlem15  8448  oeeui  8658  ersymb  8777  swoer  8794  erth  8814  boxriin  8998  boxcutc  8999  domunsncan  9138  pw2f1olem  9142  enen1  9183  enen2  9184  domen1  9185  domen2  9186  sdomen1  9187  sdomen2  9188  xpmapenlem  9210  ensymfib  9250  ordiso2  9584  wdomen1  9645  wdomen2  9646  fin23lem26  10394  fpwwe2lem7  10706  r1wunlim  10806  mul2lt0bi  13163  ixxun  13423  xov1plusxeqvd  13558  fzsplit2  13609  fseq1p1m1  13658  elfz2nn0  13675  flflp1  13858  modsubdir  13991  zesq  14275  expnngt1b  14291  hashprg  14444  hashgt0elexb  14451  hashbclem  14501  hashge2el2difb  14531  rereb  15169  rlimclim  15592  iserex  15705  caucvgb  15728  mptfzshft  15826  fsumrev  15827  climcnds  15899  fprodrev  16025  dvdsadd2b  16354  nn0ob  16432  bitsfzo  16481  dfgcd2  16593  dvdsmulgcd  16603  lcmgcdeq  16659  qden1elz  16804  mrcidb  17673  mrieqvlemd  17687  isacs2  17711  cicer  17867  ssclem  17880  issubc3  17913  ffthiso  17996  fuciso  18045  setcmon  18154  setcepi  18155  setcinv  18157  catciso  18178  acsfiindd  18623  issstrmgm  18691  mgmhmf1o  18738  issubmgm2  18741  subsubmgm  18748  resmgmhm2b  18751  issubmnd  18799  mhmf1o  18831  subsubm  18851  resmhm2b  18857  grpinvid1  19031  grpinvid2  19032  subsubg  19189  ssnmz  19206  ghmf1  19286  kerf1ghm  19287  ghmf1o  19288  conjnmzb  19293  subggim  19306  gicsubgen  19319  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmqusker  19327  gass  19341  odf1  19604  gex1  19633  fislw  19667  sylow3lem2  19670  sylow3lem6  19674  lsmdisj2a  19729  lsmdisj2b  19730  efgred2  19795  dmdprdsplit  20091  2nsgsimpgd  20146  simpgnsgbid  20147  ablsimpgd  20160  0unit  20422  irrednegb  20457  rnghmf1o  20478  rhmf1o  20517  subsubrng  20589  subrgunit  20618  subsubrg  20626  rngcinv  20659  ringcinv  20693  isdrng2  20765  issubdrg  20803  islss3  20980  islss4  20983  ellspsn6  21015  lspsneq0b  21034  islmhm2  21060  lmhmf1o  21068  reslmhm2b  21076  lssvs0or  21135  lvecinv  21138  ellspsn4  21149  lspdisjb  21151  islbs2  21179  islbs3  21180  dflidl2rng  21251  rngringbd  21341  prmirredlem  21506  islindf3  21869  lindsmm  21871  lsslindf  21873  lsslinds  21874  issubassa  21910  sraassab  21911  issubassa2  21935  gsumbagdiag  21974  subrgasclcl  22114  ply1scleq  22330  matunit  22705  slesolinvbi  22708  en2top  23013  elcls  23102  neindisj2  23152  neiptopnei  23161  neiptopreu  23162  maxlp  23176  neitr  23209  iscncl  23298  cncnp  23309  isreg2  23406  dis2ndc  23489  1stccnp  23491  islly2  23513  dislly  23526  dissnlocfin  23558  kgencmp2  23575  pt1hmeo  23835  xkocnv  23843  t0kq  23847  uffixfr  23952  flimcf  24011  cnpflf2  24029  fclscf  24054  cnextf  24095  utopsnneiplem  24277  isucn2  24309  cfilucfil  24593  psmetutop  24601  restmetu  24604  tngngp2  24694  tngngp  24696  nmoleub  24773  metdseq0  24895  cnheibor  25006  pcophtb  25081  nmoleub2lem  25166  lmmbr  25311  iscfil3  25326  cmetss  25369  cldcss  25494  mbfeqalem2  25696  mbfposb  25707  itg2const2  25796  itgss3  25870  plyco0  26251  dgrlt  26326  ulm2  26446  coseq00topi  26562  coseq0negpitopi  26563  sineq0  26584  relogbcxpb  26848  atans2  26992  xrlimcnp  27029  dchrelbas2  27299  dchrn0  27312  2sqb  27494  nosupbnd2  27779  noinfbnd2  27794  slerec  27882  sltmul2  28215  istrkg2ld  28486  tgcgreqb  28507  tgbtwncomb  28515  trgcgrg  28541  legov  28611  legov2  28612  legov3  28624  hlbtwn  28637  tglineelsb2  28658  tglinecom  28661  colline  28675  mirinv  28692  mirbtwnb  28698  mirbtwnhl  28706  perpcom  28739  isperp2  28741  oppcom  28770  opphllem3  28775  lnopp2hpgb  28789  colopp  28795  colhp  28796  lmieu  28810  iscgra1  28836  dfcgra2  28856  edgnbusgreu  29402  nb3grprlem1  29415  lfgriswlk  29724  eleclclwwlknlem2  30093  clwwlknscsh  30094  clwwlknon1  30129  numclwwlk2lem1  30408  grpoinvid1  30560  grpoinvid2  30561  leopmul  32166  hst1h  32259  bibiad  32486  eqelbid  32503  diffib  32551  ifnebib  32572  iinabrex  32591  disjabrex  32604  disjabrexf  32605  erbr3b  32639  f1o3d  32646  funimass4f  32656  2ndimaxp  32665  fgreu  32690  fcnvgreu  32691  1stpreimas  32717  fcobij  32736  resf1o  32744  nn0xmulclb  32778  fzsplit3  32799  fzo0opth  32810  eliccioo  32895  mgcmntco  32967  dfmgc2lem  32968  dfmgc2  32969  pwrssmgc  32973  mgcf1o  32976  mndlrinvb  33011  mndlactfo  33013  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  gsumhashmul  33040  ogrpinv0le  33065  ogrpaddltbi  33068  ogrpaddltrbid  33070  ogrpinv0lt  33072  cyc3genpm  33145  isarchi3  33167  prmsimpcyc  33207  domnlcanbOLD  33250  isdrng4  33264  fracerl  33273  qsxpid  33355  dvdsruasso  33378  dvdsruasso2  33379  dvdsrspss  33380  grplsmid  33397  quslsm  33398  nsgmgc  33405  nsgqusf1olem2  33407  nsgqusf1olem3  33408  pidlnzb  33415  unitpidl1  33417  elrspunidl  33421  elrspunsn  33422  drngidl  33426  drngidlhash  33427  isprmidlc  33440  prmidl0  33443  qsidom  33447  mxidlirred  33465  mxidlnzrb  33473  qsdrng  33490  rsprprmprmidlb  33516  rprmirredb  33525  deg1le0eq0  33563  ply1unit  33565  lvecdim0  33619  extdg1b  33677  irngnzply1  33691  1smat1  33750  ist0cld  33779  qtophaus  33782  reff  33785  locfinreflem  33786  cmpcref  33796  zarcls1  33815  zarclsun  33816  zarclsiin  33817  zarclssn  33819  metider  33840  pstmfval  33842  qqhval2  33928  aean  34208  imambfm  34227  eulerpartlemgvv  34341  orvcgteel  34432  orvclteel  34437  ballotlemsf1o  34478  sgn3da  34506  sgnnbi  34510  sgnpbi  34511  sgnmulsgn  34514  sgnmulsgp  34515  actfunsnf1o  34581  reprsuc  34592  reprpmtf1o  34603  sconnpi1  35207  brofs2  36041  brifs2  36042  broutsideof2  36086  bj-abv  36872  irrdiff  37292  ltflcei  37568  poimirlem25  37605  ismblfin  37621  cnambfre  37628  ftc1anclem6  37658  ismndo1  37833  isdrngo2  37918  eqvrelsymb  38562  eqvrelth  38567  lshpnelb  38940  lshpnel2N  38941  lsatspn0  38956  lsatelbN  38962  lsat0cv  38989  lcvexch  38995  lcv1  38997  lkrshp3  39062  lkrpssN  39119  lkrss2N  39125  cvlsupr2  39299  atcvrlln  39477  llncvrlpln  39515  2llnmj  39517  lplncvrlvol  39573  2lplnmj  39579  polcon2bN  39877  pcl0bN  39880  lhpmcvr3  39982  lhpmatb  39988  ltrncoidN  40085  ltrneq3  40165  ltrniotavalbN  40541  cdlemg1cN  40544  diclspsn  41151  dihopelvalcpre  41205  dihord4  41215  dihord  41221  dihmeetlem4preN  41263  dih1dimatlem0  41285  dochsscl  41325  dochoccl  41326  dochord  41327  dochsat  41340  dochshpncl  41341  dochsatshpb  41409  dochshpsat  41411  mapdval4N  41589  mapdsn  41598  hdmap14lem12  41836  hdmapip0  41872  hlhillcs  41919  riccrng  42477  ricdrng  42484  prjspner1  42581  mrefg2  42663  mzpmfp  42703  lzenom  42726  elpell14qr2  42818  elpell1qr2  42828  pellfund14b  42855  congabseq  42931  acongeq  42940  jm2.23  42953  jm2.20nn  42954  jm2.25lem1  42955  wepwsolem  42999  islssfg2  43028  lnmlmic  43045  dfacbasgrp  43065  unielss  43179  rfovcnvf1od  43966  dssmapnvod  43982  ntrclscls00  44028  rfcnpre3  44933  rfcnpre4  44934  rnmptssbi  45170  infxrgelbrnmpt  45369  xnegre  45381  xrpnf  45401  rexanuz2nf  45408  ioossioobi  45435  iccshift  45436  iocopn  45438  eliccelioc  45439  iooshift  45440  icoopn  45443  qinioo  45453  limcdm0  45539  islptre  45540  islpcn  45560  limcresioolb  45564  climuzlem  45664  climlimsup  45681  liminfgelimsup  45703  liminfgelimsupuz  45709  climliminf  45727  climliminflimsup  45729  climliminflimsup2  45730  xlimpnfxnegmnf  45735  xlimbr  45748  xlimmnfv  45755  xlimpnfv  45759  xlimclim2  45761  dfxlim2v  45768  climresdm  45771  xlimresdm  45780  xlimliminflimsup  45783  fperdvper  45840  itgperiod  45902  fourierdlem32  46060  fourierdlem33  46061  fourierdlem48  46075  fourierdlem49  46076  fourierdlem71  46098  fourierdlem81  46108  preimagelt  46620  preimalegt  46621  smfliminflem  46751  smfliminfmpt  46753  fcoresfob  46987  m1mod0mod1  47243  uspgrimprop  47757  rngcinvALTV  47999  ringcinvALTV  48033  fvconstr  48569  fvconstrn0  48570  lubeldm2  48636  glbeldm2  48637  functhinclem1  48708  fullthinc  48713  thinciso  48727  prstchom2ALT  48746