Theorem impbida 826

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  eqrdav  2816  frsn  5404  funfvbrb  6561  iinpreima  6576  frnssb  6622  fnprb  6706  fntpb  6707  fpr2g  6709  nvocnv  6770  fsnex  6771  f1prex  6772  f1ocnv2d  7125  el2xptp0  7453  1stconst  7508  2ndconst  7509  cnvf1o  7519  tfrlem15  7733  oeeui  7928  ersymb  8002  swoer  8018  erth  8035  boxriin  8196  boxcutc  8197  domunsncan  8308  pw2f1olem  8312  enen1  8348  enen2  8349  domen1  8350  domen2  8351  sdomen1  8352  sdomen2  8353  xpmapenlem  8375  ordiso2  8668  wdomen1  8729  wdomen2  8730  fin23lem26  9441  fpwwe2lem8  9753  r1wunlim  9853  mul2lt0bi  12169  ixxun  12428  xov1plusxeqvd  12560  fzsplit2  12608  fseq1p1m1  12656  elfz2nn0  12673  flflp1  12851  modsubdir  12982  zesq  13229  hashprg  13419  hashgt0elexb  13426  hashbclem  13472  hashge2el2difb  13500  rereb  14102  rlimclim  14519  iserex  14629  caucvgb  14652  mptfzshft  14751  fsumrev  14752  climcnds  14824  fprodrev  14947  dvdsadd2b  15270  nn0ob  15339  bitsfzo  15395  dfgcd2  15501  dvdsmulgcd  15512  lcmgcdeq  15563  qden1elz  15701  mrcidb  16499  mrieqvlemd  16513  isacs2  16537  cicer  16689  ssclem  16702  issubc3  16732  ffthiso  16812  fuciso  16858  setcmon  16960  setcepi  16961  setcinv  16963  catciso  16980  acsfiindd  17401  issstrmgm  17476  issubmnd  17542  mhmf1o  17569  subsubm  17581  resmhm2b  17585  grpinvid1  17694  grpinvid2  17695  subsubg  17838  ssnmz  17857  ghmf1  17910  ghmf1o  17911  conjnmzb  17916  subggim  17929  gicsubgen  17941  gass  17954  odf1  18199  gex1  18226  fislw  18260  sylow3lem2  18263  sylow3lem6  18267  lsmdisj2a  18320  lsmdisj2b  18321  efgred2  18386  dmdprdsplit  18667  0unit  18901  irrednegb  18932  rhmf1o  18955  kerf1hrm  18966  isdrng2  18980  subrgunit  19021  issubdrg  19028  subsubrg  19029  islss3  19185  islss4  19188  lspsnel6  19220  lspsneq0b  19239  islmhm2  19264  lmhmf1o  19272  reslmhm2b  19280  lssvs0or  19336  lvecinv  19339  lspsnel4  19350  lspdisjb  19352  islbs2  19382  islbs3  19383  issubassa  19552  issubassa2  19573  gsumbagdiag  19604  subrgasclcl  19726  prmirredlem  20068  islindf3  20395  lindsmm  20397  lsslindf  20399  lsslinds  20400  matunit  20716  slesolinvbi  20719  en2top  21023  elcls  21111  neindisj2  21161  neiptopnei  21170  neiptopreu  21171  maxlp  21185  neitr  21218  iscncl  21307  cncnp  21318  isreg2  21415  dis2ndc  21497  1stccnp  21499  islly2  21521  dislly  21534  dissnlocfin  21566  kgencmp2  21583  pt1hmeo  21843  xkocnv  21851  t0kq  21855  uffixfr  21960  flimcf  22019  cnpflf2  22037  fclscf  22062  cnextf  22103  utopsnneiplem  22284  isucn2  22316  cfilucfil  22597  psmetutop  22605  restmetu  22608  tngngp2  22689  tngngp  22691  nmoleub  22768  metdseq0  22890  cnheibor  22987  pcophtb  23061  nmoleub2lem  23146  lmmbr  23289  iscfil3  23304  cmetss  23346  cldcss  23446  mbfeqalem2  23645  mbfposb  23656  itg2const2  23744  itgss3  23817  plyco0  24184  dgrlt  24258  ulm2  24375  coseq00topi  24491  coseq0negpitopi  24492  sineq0  24510  relogbcxpb  24761  atans2  24894  xrlimcnp  24931  dchrelbas2  25198  dchrn0  25211  2sqb  25393  istrkg2ld  25595  tgcgreqb  25612  tgbtwncomb  25620  trgcgrg  25646  legov  25716  legov2  25717  legov3  25729  hlbtwn  25742  tglineelsb2  25763  tglinecom  25766  colline  25780  mirinv  25797  mirbtwnb  25803  mirbtwnhl  25811  perpcom  25844  isperp2  25846  oppcom  25872  opphllem3  25877  lnopp2hpgb  25891  colopp  25897  colhp  25898  lmieu  25912  iscgra1  25938  dfcgra2  25957  edgnbusgreu  26506  edgnbusgreuOLD  26507  nb3grprlem1  26520  lfgriswlk  26835  eleclclwwlknlem2  27234  clwwlknscsh  27235  clwwlknon1  27287  numclwwlk2lem1  27578  numclwwlk2lem1OLD  27585  grpoinvid1  27733  grpoinvid2  27734  leopmul  29343  hst1h  29436  disjabrex  29742  disjabrexf  29743  erbr3b  29776  f1o3d  29780  funimass4f  29786  fgreu  29820  fcnvgreu  29821  1stpreimas  29832  fcobij  29849  resf1o  29854  fzsplit3  29902  eliccioo  29986  ogrpinv0le  30063  ogrpaddltbi  30066  ogrpaddltrbid  30068  ogrpinv0lt  30070  isarchi3  30088  1smat1  30217  fimaproj  30247  qtophaus  30250  reff  30253  locfinreflem  30254  cmpcref  30264  metider  30284  pstmfval  30286  qqhval2  30373  aean  30654  imambfm  30671  eulerpartlemgvv  30785  orvcgteel  30876  orvclteel  30881  ballotlemsf1o  30922  sgn3da  30950  sgnnbi  30954  sgnpbi  30955  sgnmulsgn  30958  sgnmulsgp  30959  actfunsnf1o  31029  reprsuc  31040  reprpmtf1o  31051  sconnpi1  31565  nosupbnd2  32204  slerec  32265  brofs2  32526  brifs2  32527  broutsideof2  32571  ltflcei  33728  poimirlem25  33765  ismblfin  33781  cnambfre  33788  ftc1anclem6  33820  ismndo1  34001  isdrngo2  34086  lshpnelb  34782  lshpnel2N  34783  lsatspn0  34798  lsatelbN  34804  lsat0cv  34831  lcvexch  34837  lcv1  34839  lkrshp3  34904  lkrpssN  34961  lkrss2N  34967  cvlsupr2  35141  atcvrlln  35318  llncvrlpln  35356  2llnmj  35358  lplncvrlvol  35414  2lplnmj  35420  polcon2bN  35718  pcl0bN  35721  lhpmcvr3  35823  lhpmatb  35829  ltrncoidN  35926  ltrneq3  36006  ltrniotavalbN  36382  cdlemg1cN  36385  diclspsn  36992  dihopelvalcpre  37046  dihord4  37056  dihord  37062  dihmeetlem4preN  37104  dih1dimatlem0  37126  dochsscl  37166  dochoccl  37167  dochord  37168  dochsat  37181  dochshpncl  37182  dochsatshpb  37250  dochshpsat  37252  mapdval4N  37430  mapdsn  37439  hdmap14lem12  37677  hdmapip0  37713  hlhillcs  37756  mrefg2  37789  mzpmfp  37829  lzenom  37852  elpell14qr2  37945  elpell1qr2  37955  pellfund14b  37982  congabseq  38059  acongeq  38068  jm2.23  38081  jm2.20nn  38082  jm2.25lem1  38083  wepwsolem  38130  islssfg2  38159  lnmlmic  38176  dfacbasgrp  38196  rfovcnvf1od  38815  dssmapnvod  38831  ntrclscls00  38881  rfcnpre3  39703  rfcnpre4  39704  rnmptssbi  39977  infxrgelbrnmpt  40179  xnegre  40192  xrpnf  40212  ioossioobi  40241  iccshift  40242  iocopn  40244  eliccelioc  40245  iooshift  40246  icoopn  40249  qinioo  40259  limcdm0  40347  islptre  40348  islpcn  40368  limcresioolb  40372  climuzlem  40472  climlimsup  40489  liminfgelimsup  40511  liminfgelimsupuz  40517  climliminf  40535  climliminflimsup  40537  climliminflimsup2  40538  xlimbr  40550  xlimmnfv  40557  xlimpnfv  40561  xlimclim2  40563  dfxlim2v  40570  fperdvper  40630  itgperiod  40693  fourierdlem32  40852  fourierdlem33  40853  fourierdlem48  40867  fourierdlem49  40868  fourierdlem71  40890  fourierdlem81  40900  smfliminflem  41535  smfliminfmpt  41537  m1mod0mod1  41931  mgmhmf1o  42372  issubmgm2  42375  subsubmgm  42382  resmgmhm2b  42385  rnghmf1o  42488  rngcinv  42566  rngcinvALTV  42578  ringcinv  42617  ringcinvALTV  42641