Theorem impbida 798

Description: Deduce an equivalence from two implications. Variant of impbid 211. (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 413	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 413	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 211	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  biadanid  820  eqrdav  2738  frsn  5675  funfvbrb  6937  iinpreima  6955  frnssb  7004  fnprb  7093  fntpb  7094  fpr2g  7096  nvocnv  7162  fsnex  7164  f1ocnv2d  7531  el2xptp0  7887  1stconst  7949  2ndconst  7950  cnvf1o  7960  fimaproj  7985  tfrlem15  8232  oeeui  8442  ersymb  8521  swoer  8537  erth  8556  boxriin  8737  boxcutc  8738  domunsncan  8868  pw2f1olem  8872  enen1  8913  enen2  8914  domen1  8915  domen2  8916  sdomen1  8917  sdomen2  8918  xpmapenlem  8940  ensymfib  8979  ordiso2  9283  wdomen1  9344  wdomen2  9345  fin23lem26  10090  fpwwe2lem7  10402  r1wunlim  10502  mul2lt0bi  12845  ixxun  13104  xov1plusxeqvd  13239  fzsplit2  13290  fseq1p1m1  13339  elfz2nn0  13356  flflp1  13536  modsubdir  13669  zesq  13950  expnngt1b  13966  hashprg  14119  hashgt0elexb  14126  hashbclem  14173  hashge2el2difb  14205  rereb  14840  rlimclim  15264  iserex  15377  caucvgb  15400  mptfzshft  15499  fsumrev  15500  climcnds  15572  fprodrev  15696  dvdsadd2b  16024  nn0ob  16102  bitsfzo  16151  dfgcd2  16263  dvdsmulgcd  16274  lcmgcdeq  16326  qden1elz  16470  mrcidb  17333  mrieqvlemd  17347  isacs2  17371  cicer  17527  ssclem  17540  issubc3  17573  ffthiso  17654  fuciso  17702  setcmon  17811  setcepi  17812  setcinv  17814  catciso  17835  acsfiindd  18280  issstrmgm  18346  issubmnd  18421  mhmf1o  18449  subsubm  18464  resmhm2b  18470  grpinvid1  18639  grpinvid2  18640  subsubg  18787  ssnmz  18803  ghmf1  18872  ghmf1o  18873  conjnmzb  18878  subggim  18891  gicsubgen  18903  gass  18916  odf1  19178  gex1  19205  fislw  19239  sylow3lem2  19242  sylow3lem6  19246  lsmdisj2a  19302  lsmdisj2b  19303  efgred2  19368  dmdprdsplit  19659  2nsgsimpgd  19714  simpgnsgbid  19715  ablsimpgd  19728  0unit  19931  irrednegb  19962  rhmf1o  19985  kerf1ghm  19996  isdrng2  20010  subrgunit  20051  issubdrg  20058  subsubrg  20059  islss3  20230  islss4  20233  lspsnel6  20265  lspsneq0b  20284  islmhm2  20309  lmhmf1o  20317  reslmhm2b  20325  lssvs0or  20381  lvecinv  20384  lspsnel4  20395  lspdisjb  20397  islbs2  20425  islbs3  20426  prmirredlem  20703  islindf3  21042  lindsmm  21044  lsslindf  21046  lsslinds  21047  issubassa  21082  issubassa2  21105  gsumbagdiagOLD  21151  gsumbagdiag  21154  subrgasclcl  21284  matunit  21836  slesolinvbi  21839  en2top  22144  elcls  22233  neindisj2  22283  neiptopnei  22292  neiptopreu  22293  maxlp  22307  neitr  22340  iscncl  22429  cncnp  22440  isreg2  22537  dis2ndc  22620  1stccnp  22622  islly2  22644  dislly  22657  dissnlocfin  22689  kgencmp2  22706  pt1hmeo  22966  xkocnv  22974  t0kq  22978  uffixfr  23083  flimcf  23142  cnpflf2  23160  fclscf  23185  cnextf  23226  utopsnneiplem  23408  isucn2  23440  cfilucfil  23724  psmetutop  23732  restmetu  23735  tngngp2  23825  tngngp  23827  nmoleub  23904  metdseq0  24026  cnheibor  24127  pcophtb  24201  nmoleub2lem  24286  lmmbr  24431  iscfil3  24446  cmetss  24489  cldcss  24614  mbfeqalem2  24815  mbfposb  24826  itg2const2  24915  itgss3  24988  plyco0  25362  dgrlt  25436  ulm2  25553  coseq00topi  25668  coseq0negpitopi  25669  sineq0  25689  relogbcxpb  25946  atans2  26090  xrlimcnp  26127  dchrelbas2  26394  dchrn0  26407  2sqb  26589  istrkg2ld  26830  tgcgreqb  26851  tgbtwncomb  26859  trgcgrg  26885  legov  26955  legov2  26956  legov3  26968  hlbtwn  26981  tglineelsb2  27002  tglinecom  27005  colline  27019  mirinv  27036  mirbtwnb  27042  mirbtwnhl  27050  perpcom  27083  isperp2  27085  oppcom  27114  opphllem3  27119  lnopp2hpgb  27133  colopp  27139  colhp  27140  lmieu  27154  iscgra1  27180  dfcgra2  27200  edgnbusgreu  27743  nb3grprlem1  27756  lfgriswlk  28065  eleclclwwlknlem2  28434  clwwlknscsh  28435  clwwlknon1  28470  numclwwlk2lem1  28749  grpoinvid1  28899  grpoinvid2  28900  leopmul  30505  hst1h  30598  diffib  30878  eqsnd  30886  iinabrex  30917  disjabrex  30930  disjabrexf  30931  erbr3b  30966  f1o3d  30971  funimass4f  30981  2ndimaxp  30993  fgreu  31018  fcnvgreu  31019  1stpreimas  31047  fcobij  31066  resf1o  31074  nn0xmulclb  31103  fzsplit3  31124  eliccioo  31214  mgcmntco  31281  dfmgc2lem  31282  dfmgc2  31283  pwrssmgc  31287  mgcf1o  31290  gsumhashmul  31325  ogrpinv0le  31350  ogrpaddltbi  31353  ogrpaddltrbid  31355  ogrpinv0lt  31357  cyc3genpm  31428  isarchi3  31450  prmsimpcyc  31490  qsxpid  31567  grplsmid  31601  quslsm  31602  nsgmgc  31606  nsgqusf1olem2  31608  nsgqusf1olem3  31609  elrspunidl  31615  isprmidlc  31632  prmidl0  31635  qsidom  31639  mxidlnzrb  31653  ply1scleq  31677  lvecdim0  31699  extdg1b  31748  1smat1  31763  ist0cld  31792  qtophaus  31795  reff  31798  locfinreflem  31799  cmpcref  31809  zarcls1  31828  zarclsun  31829  zarclsiin  31830  zarclssn  31832  metider  31853  pstmfval  31855  qqhval2  31941  aean  32221  imambfm  32238  eulerpartlemgvv  32352  orvcgteel  32443  orvclteel  32448  ballotlemsf1o  32489  sgn3da  32517  sgnnbi  32521  sgnpbi  32522  sgnmulsgn  32525  sgnmulsgp  32526  actfunsnf1o  32593  reprsuc  32604  reprpmtf1o  32615  sconnpi1  33210  nosupbnd2  33928  noinfbnd2  33943  slerec  34022  brofs2  34388  brifs2  34389  broutsideof2  34433  bj-abv  35100  irrdiff  35506  ltflcei  35774  poimirlem25  35811  ismblfin  35827  cnambfre  35834  ftc1anclem6  35864  ismndo1  36040  isdrngo2  36125  eqvrelsymb  36726  eqvrelth  36731  lshpnelb  37005  lshpnel2N  37006  lsatspn0  37021  lsatelbN  37027  lsat0cv  37054  lcvexch  37060  lcv1  37062  lkrshp3  37127  lkrpssN  37184  lkrss2N  37190  cvlsupr2  37364  atcvrlln  37541  llncvrlpln  37579  2llnmj  37581  lplncvrlvol  37637  2lplnmj  37643  polcon2bN  37941  pcl0bN  37944  lhpmcvr3  38046  lhpmatb  38052  ltrncoidN  38149  ltrneq3  38229  ltrniotavalbN  38605  cdlemg1cN  38608  diclspsn  39215  dihopelvalcpre  39269  dihord4  39279  dihord  39285  dihmeetlem4preN  39327  dih1dimatlem0  39349  dochsscl  39389  dochoccl  39390  dochord  39391  dochsat  39404  dochshpncl  39405  dochsatshpb  39473  dochshpsat  39475  mapdval4N  39653  mapdsn  39662  hdmap14lem12  39900  hdmapip0  39936  hlhillcs  39983  prjspner1  40470  mrefg2  40536  mzpmfp  40576  lzenom  40599  elpell14qr2  40691  elpell1qr2  40701  pellfund14b  40728  congabseq  40803  acongeq  40812  jm2.23  40825  jm2.20nn  40826  jm2.25lem1  40827  wepwsolem  40874  islssfg2  40903  lnmlmic  40920  dfacbasgrp  40940  rfovcnvf1od  41619  dssmapnvod  41635  ntrclscls00  41683  rfcnpre3  42583  rfcnpre4  42584  rnmptssbi  42814  infxrgelbrnmpt  43001  xnegre  43013  xrpnf  43033  ioossioobi  43062  iccshift  43063  iocopn  43065  eliccelioc  43066  iooshift  43067  icoopn  43070  qinioo  43080  limcdm0  43166  islptre  43167  islpcn  43187  limcresioolb  43191  climuzlem  43291  climlimsup  43308  liminfgelimsup  43330  liminfgelimsupuz  43336  climliminf  43354  climliminflimsup  43356  climliminflimsup2  43357  xlimpnfxnegmnf  43362  xlimbr  43375  xlimmnfv  43382  xlimpnfv  43386  xlimclim2  43388  dfxlim2v  43395  climresdm  43398  xlimresdm  43407  xlimliminflimsup  43410  fperdvper  43467  itgperiod  43529  fourierdlem32  43687  fourierdlem33  43688  fourierdlem48  43702  fourierdlem49  43703  fourierdlem71  43725  fourierdlem81  43735  preimagelt  44244  preimalegt  44245  smfliminflem  44374  smfliminfmpt  44376  fcoresfob  44577  m1mod0mod1  44832  mgmhmf1o  45352  issubmgm2  45355  subsubmgm  45362  resmgmhm2b  45365  rnghmf1o  45472  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  fvconstr  46194  fvconstrn0  46195  lubeldm2  46261  glbeldm2  46262  functhinclem1  46333  fullthinc  46338  thinciso  46352  prstchom2ALT  46371