Theorem impbida 797

Description: Deduce an equivalence from two implications. Variant of impbid 213. (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 213	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  eqrdav  2794  frsn  5525  funfvbrb  6686  iinpreima  6702  frnssb  6748  fnprb  6837  fntpb  6838  fpr2g  6840  nvocnv  6903  fsnex  6904  f1ocnv2d  7256  el2xptp0  7592  1stconst  7651  2ndconst  7652  cnvf1o  7662  tfrlem15  7880  oeeui  8078  ersymb  8153  swoer  8169  erth  8188  boxriin  8352  boxcutc  8353  domunsncan  8464  pw2f1olem  8468  enen1  8504  enen2  8505  domen1  8506  domen2  8507  sdomen1  8508  sdomen2  8509  xpmapenlem  8531  ordiso2  8825  wdomen1  8886  wdomen2  8887  fin23lem26  9593  fpwwe2lem8  9905  r1wunlim  10005  mul2lt0bi  12345  ixxun  12604  xov1plusxeqvd  12734  fzsplit2  12782  fseq1p1m1  12831  elfz2nn0  12848  flflp1  13027  modsubdir  13158  zesq  13437  expnngt1b  13453  hashprg  13604  hashgt0elexb  13611  hashbclem  13658  hashge2el2difb  13686  rereb  14313  rlimclim  14737  iserex  14847  caucvgb  14870  mptfzshft  14966  fsumrev  14967  climcnds  15039  fprodrev  15164  dvdsadd2b  15489  nn0ob  15568  bitsfzo  15617  dfgcd2  15723  dvdsmulgcd  15734  lcmgcdeq  15785  qden1elz  15926  mrcidb  16715  mrieqvlemd  16729  isacs2  16753  cicer  16905  ssclem  16918  issubc3  16948  ffthiso  17028  fuciso  17074  setcmon  17176  setcepi  17177  setcinv  17179  catciso  17196  acsfiindd  17616  issstrmgm  17691  issubmnd  17757  mhmf1o  17784  subsubm  17796  resmhm2b  17800  grpinvid1  17911  grpinvid2  17912  subsubg  18056  ssnmz  18075  ghmf1  18128  ghmf1o  18129  conjnmzb  18134  subggim  18147  gicsubgen  18159  gass  18172  odf1  18419  gex1  18446  fislw  18480  sylow3lem2  18483  sylow3lem6  18487  lsmdisj2a  18540  lsmdisj2b  18541  efgred2  18606  dmdprdsplit  18886  0unit  19120  irrednegb  19151  rhmf1o  19174  kerf1ghm  19187  kerf1hrmOLD  19188  isdrng2  19202  subrgunit  19243  issubdrg  19250  subsubrg  19251  islss3  19421  islss4  19424  lspsnel6  19456  lspsneq0b  19475  islmhm2  19500  lmhmf1o  19508  reslmhm2b  19516  lssvs0or  19572  lvecinv  19575  lspsnel4  19586  lspdisjb  19588  islbs2  19616  islbs3  19617  issubassa  19786  issubassa2  19813  gsumbagdiag  19844  subrgasclcl  19966  prmirredlem  20322  islindf3  20652  lindsmm  20654  lsslindf  20656  lsslinds  20657  matunit  20971  slesolinvbi  20974  en2top  21277  elcls  21365  neindisj2  21415  neiptopnei  21424  neiptopreu  21425  maxlp  21439  neitr  21472  iscncl  21561  cncnp  21572  isreg2  21669  dis2ndc  21752  1stccnp  21754  islly2  21776  dislly  21789  dissnlocfin  21821  kgencmp2  21838  pt1hmeo  22098  xkocnv  22106  t0kq  22110  uffixfr  22215  flimcf  22274  cnpflf2  22292  fclscf  22317  cnextf  22358  utopsnneiplem  22539  isucn2  22571  cfilucfil  22852  psmetutop  22860  restmetu  22863  tngngp2  22944  tngngp  22946  nmoleub  23023  metdseq0  23145  cnheibor  23242  pcophtb  23316  nmoleub2lem  23401  lmmbr  23544  iscfil3  23559  cmetss  23602  cldcss  23727  mbfeqalem2  23926  mbfposb  23937  itg2const2  24025  itgss3  24098  plyco0  24465  dgrlt  24539  ulm2  24656  coseq00topi  24771  coseq0negpitopi  24772  sineq0  24792  relogbcxpb  25046  atans2  25190  xrlimcnp  25228  dchrelbas2  25495  dchrn0  25508  2sqb  25690  istrkg2ld  25928  tgcgreqb  25949  tgbtwncomb  25957  trgcgrg  25983  legov  26053  legov2  26054  legov3  26066  hlbtwn  26079  tglineelsb2  26100  tglinecom  26103  colline  26117  mirinv  26134  mirbtwnb  26140  mirbtwnhl  26148  perpcom  26181  isperp2  26183  oppcom  26212  opphllem3  26217  lnopp2hpgb  26231  colopp  26237  colhp  26238  lmieu  26252  iscgra1  26278  dfcgra2  26298  edgnbusgreu  26832  nb3grprlem1  26845  lfgriswlk  27155  eleclclwwlknlem2  27527  clwwlknscsh  27528  clwwlknon1  27563  numclwwlk2lem1  27847  grpoinvid1  27996  grpoinvid2  27997  leopmul  29602  hst1h  29695  eqsnd  29978  disjabrex  30022  disjabrexf  30023  erbr3b  30058  f1o3d  30062  funimass4f  30072  fgreu  30107  fcnvgreu  30108  1stpreimas  30129  fcobij  30146  resf1o  30154  nn0xmulclb  30184  fzsplit3  30203  eliccioo  30291  ogrpinv0le  30376  ogrpaddltbi  30379  ogrpaddltrbid  30381  ogrpinv0lt  30383  cyc3genpm  30432  isarchi3  30454  lvecdim0  30609  extdg1b  30658  1smat1  30684  fimaproj  30714  qtophaus  30717  reff  30720  locfinreflem  30721  cmpcref  30731  metider  30751  pstmfval  30753  qqhval2  30840  aean  31120  imambfm  31137  eulerpartlemgvv  31251  orvcgteel  31342  orvclteel  31347  ballotlemsf1o  31388  sgn3da  31416  sgnnbi  31420  sgnpbi  31421  sgnmulsgn  31424  sgnmulsgp  31425  actfunsnf1o  31492  reprsuc  31503  reprpmtf1o  31514  sconnpi1  32094  nosupbnd2  32825  slerec  32886  brofs2  33147  brifs2  33148  broutsideof2  33192  ltflcei  34411  poimirlem25  34448  ismblfin  34464  cnambfre  34471  ftc1anclem6  34503  ismndo1  34683  isdrngo2  34768  eqvrelsymb  35372  eqvrelth  35377  lshpnelb  35651  lshpnel2N  35652  lsatspn0  35667  lsatelbN  35673  lsat0cv  35700  lcvexch  35706  lcv1  35708  lkrshp3  35773  lkrpssN  35830  lkrss2N  35836  cvlsupr2  36010  atcvrlln  36187  llncvrlpln  36225  2llnmj  36227  lplncvrlvol  36283  2lplnmj  36289  polcon2bN  36587  pcl0bN  36590  lhpmcvr3  36692  lhpmatb  36698  ltrncoidN  36795  ltrneq3  36875  ltrniotavalbN  37251  cdlemg1cN  37254  diclspsn  37861  dihopelvalcpre  37915  dihord4  37925  dihord  37931  dihmeetlem4preN  37973  dih1dimatlem0  37995  dochsscl  38035  dochoccl  38036  dochord  38037  dochsat  38050  dochshpncl  38051  dochsatshpb  38119  dochshpsat  38121  mapdval4N  38299  mapdsn  38308  hdmap14lem12  38546  hdmapip0  38582  hlhillcs  38625  mrefg2  38789  mzpmfp  38829  lzenom  38852  elpell14qr2  38944  elpell1qr2  38954  pellfund14b  38981  congabseq  39056  acongeq  39065  jm2.23  39078  jm2.20nn  39079  jm2.25lem1  39080  wepwsolem  39127  islssfg2  39156  lnmlmic  39173  dfacbasgrp  39193  rfovcnvf1od  39835  dssmapnvod  39851  ntrclscls00  39901  2nsgsimpgd  40158  simpgnsgbid  40159  ablsimpgd  40173  prmsimpcyc  40174  rfcnpre3  40829  rfcnpre4  40830  rnmptssbi  41075  infxrgelbrnmpt  41272  xnegre  41284  xrpnf  41304  ioossioobi  41335  iccshift  41336  iocopn  41338  eliccelioc  41339  iooshift  41340  icoopn  41343  qinioo  41353  limcdm0  41441  islptre  41442  islpcn  41462  limcresioolb  41466  climuzlem  41566  climlimsup  41583  liminfgelimsup  41605  liminfgelimsupuz  41611  climliminf  41629  climliminflimsup  41631  climliminflimsup2  41632  xlimpnfxnegmnf  41637  xlimbr  41650  xlimmnfv  41657  xlimpnfv  41661  xlimclim2  41663  dfxlim2v  41670  climresdm  41673  xlimresdm  41682  xlimliminflimsup  41685  fperdvper  41744  itgperiod  41807  fourierdlem32  41966  fourierdlem33  41967  fourierdlem48  41981  fourierdlem49  41982  fourierdlem71  42004  fourierdlem81  42014  preimagelt  42522  preimalegt  42523  smfliminflem  42646  smfliminfmpt  42648  m1mod0mod1  43045  mgmhmf1o  43536  issubmgm2  43539  subsubmgm  43546  resmgmhm2b  43549  rnghmf1o  43652  rngcinv  43730  rngcinvALTV  43742  ringcinv  43781  ringcinvALTV  43805