Theorem impbida 799

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  eqrdav  2823  frsn  5642  funfvbrb  6824  iinpreima  6840  frnssb  6888  fnprb  6974  fntpb  6975  fpr2g  6977  nvocnv  7041  fsnex  7042  f1ocnv2d  7401  el2xptp0  7739  1stconst  7798  2ndconst  7799  cnvf1o  7809  fimaproj  7832  tfrlem15  8031  oeeui  8231  ersymb  8306  swoer  8322  erth  8341  boxriin  8507  boxcutc  8508  domunsncan  8620  pw2f1olem  8624  enen1  8660  enen2  8661  domen1  8662  domen2  8663  sdomen1  8664  sdomen2  8665  xpmapenlem  8687  ordiso2  8982  wdomen1  9043  wdomen2  9044  fin23lem26  9750  fpwwe2lem8  10062  r1wunlim  10162  mul2lt0bi  12498  ixxun  12757  xov1plusxeqvd  12887  fzsplit2  12935  fseq1p1m1  12984  elfz2nn0  13001  flflp1  13180  modsubdir  13311  zesq  13590  expnngt1b  13606  hashprg  13759  hashgt0elexb  13766  hashbclem  13813  hashge2el2difb  13843  rereb  14482  rlimclim  14906  iserex  15016  caucvgb  15039  mptfzshft  15136  fsumrev  15137  climcnds  15209  fprodrev  15334  dvdsadd2b  15659  nn0ob  15738  bitsfzo  15787  dfgcd2  15897  dvdsmulgcd  15908  lcmgcdeq  15959  qden1elz  16100  mrcidb  16889  mrieqvlemd  16903  isacs2  16927  cicer  17079  ssclem  17092  issubc3  17122  ffthiso  17202  fuciso  17248  setcmon  17350  setcepi  17351  setcinv  17353  catciso  17370  acsfiindd  17790  issstrmgm  17866  issubmnd  17941  mhmf1o  17969  subsubm  17984  resmhm2b  17990  grpinvid1  18157  grpinvid2  18158  subsubg  18305  ssnmz  18321  ghmf1  18390  ghmf1o  18391  conjnmzb  18396  subggim  18409  gicsubgen  18421  gass  18434  odf1  18692  gex1  18719  fislw  18753  sylow3lem2  18756  sylow3lem6  18760  lsmdisj2a  18816  lsmdisj2b  18817  efgred2  18882  dmdprdsplit  19172  2nsgsimpgd  19227  simpgnsgbid  19228  ablsimpgd  19241  0unit  19433  irrednegb  19464  rhmf1o  19487  kerf1ghm  19500  kerf1hrmOLD  19501  isdrng2  19515  subrgunit  19556  issubdrg  19563  subsubrg  19564  islss3  19734  islss4  19737  lspsnel6  19769  lspsneq0b  19788  islmhm2  19813  lmhmf1o  19821  reslmhm2b  19829  lssvs0or  19885  lvecinv  19888  lspsnel4  19899  lspdisjb  19901  islbs2  19929  islbs3  19930  issubassa  20101  issubassa2  20124  gsumbagdiag  20159  subrgasclcl  20282  prmirredlem  20643  islindf3  20973  lindsmm  20975  lsslindf  20977  lsslinds  20978  matunit  21290  slesolinvbi  21293  en2top  21596  elcls  21684  neindisj2  21734  neiptopnei  21743  neiptopreu  21744  maxlp  21758  neitr  21791  iscncl  21880  cncnp  21891  isreg2  21988  dis2ndc  22071  1stccnp  22073  islly2  22095  dislly  22108  dissnlocfin  22140  kgencmp2  22157  pt1hmeo  22417  xkocnv  22425  t0kq  22429  uffixfr  22534  flimcf  22593  cnpflf2  22611  fclscf  22636  cnextf  22677  utopsnneiplem  22859  isucn2  22891  cfilucfil  23172  psmetutop  23180  restmetu  23183  tngngp2  23264  tngngp  23266  nmoleub  23343  metdseq0  23465  cnheibor  23562  pcophtb  23636  nmoleub2lem  23721  lmmbr  23864  iscfil3  23879  cmetss  23922  cldcss  24047  mbfeqalem2  24246  mbfposb  24257  itg2const2  24345  itgss3  24418  plyco0  24785  dgrlt  24859  ulm2  24976  coseq00topi  25091  coseq0negpitopi  25092  sineq0  25112  relogbcxpb  25368  atans2  25512  xrlimcnp  25549  dchrelbas2  25816  dchrn0  25829  2sqb  26011  istrkg2ld  26249  tgcgreqb  26270  tgbtwncomb  26278  trgcgrg  26304  legov  26374  legov2  26375  legov3  26387  hlbtwn  26400  tglineelsb2  26421  tglinecom  26424  colline  26438  mirinv  26455  mirbtwnb  26461  mirbtwnhl  26469  perpcom  26502  isperp2  26504  oppcom  26533  opphllem3  26538  lnopp2hpgb  26552  colopp  26558  colhp  26559  lmieu  26573  iscgra1  26599  dfcgra2  26619  edgnbusgreu  27152  nb3grprlem1  27165  lfgriswlk  27473  eleclclwwlknlem2  27843  clwwlknscsh  27844  clwwlknon1  27879  numclwwlk2lem1  28158  grpoinvid1  28308  grpoinvid2  28309  leopmul  29914  hst1h  30007  eqsnd  30292  disjabrex  30335  disjabrexf  30336  erbr3b  30371  f1o3d  30375  funimass4f  30385  fgreu  30420  fcnvgreu  30421  1stpreimas  30444  fcobij  30461  resf1o  30469  nn0xmulclb  30499  fzsplit3  30520  eliccioo  30611  ogrpinv0le  30720  ogrpaddltbi  30723  ogrpaddltrbid  30725  ogrpinv0lt  30727  cyc3genpm  30798  isarchi3  30820  prmsimpcyc  30860  qsxpid  30931  isprmidlc  30967  qsidom  30971  mxidlnzrb  30985  lvecdim0  31009  extdg1b  31058  1smat1  31073  qtophaus  31104  reff  31107  locfinreflem  31108  cmpcref  31118  metider  31138  pstmfval  31140  qqhval2  31227  aean  31507  imambfm  31524  eulerpartlemgvv  31638  orvcgteel  31729  orvclteel  31734  ballotlemsf1o  31775  sgn3da  31803  sgnnbi  31807  sgnpbi  31808  sgnmulsgn  31811  sgnmulsgp  31812  actfunsnf1o  31879  reprsuc  31890  reprpmtf1o  31901  sconnpi1  32490  nosupbnd2  33220  slerec  33281  brofs2  33542  brifs2  33543  broutsideof2  33587  ltflcei  34884  poimirlem25  34921  ismblfin  34937  cnambfre  34944  ftc1anclem6  34976  ismndo1  35155  isdrngo2  35240  eqvrelsymb  35845  eqvrelth  35850  lshpnelb  36124  lshpnel2N  36125  lsatspn0  36140  lsatelbN  36146  lsat0cv  36173  lcvexch  36179  lcv1  36181  lkrshp3  36246  lkrpssN  36303  lkrss2N  36309  cvlsupr2  36483  atcvrlln  36660  llncvrlpln  36698  2llnmj  36700  lplncvrlvol  36756  2lplnmj  36762  polcon2bN  37060  pcl0bN  37063  lhpmcvr3  37165  lhpmatb  37171  ltrncoidN  37268  ltrneq3  37348  ltrniotavalbN  37724  cdlemg1cN  37727  diclspsn  38334  dihopelvalcpre  38388  dihord4  38398  dihord  38404  dihmeetlem4preN  38446  dih1dimatlem0  38468  dochsscl  38508  dochoccl  38509  dochord  38510  dochsat  38523  dochshpncl  38524  dochsatshpb  38592  dochshpsat  38594  mapdval4N  38772  mapdsn  38781  hdmap14lem12  39019  hdmapip0  39055  hlhillcs  39098  mrefg2  39310  mzpmfp  39350  lzenom  39373  elpell14qr2  39465  elpell1qr2  39475  pellfund14b  39502  congabseq  39577  acongeq  39586  jm2.23  39599  jm2.20nn  39600  jm2.25lem1  39601  wepwsolem  39648  islssfg2  39677  lnmlmic  39694  dfacbasgrp  39714  rfovcnvf1od  40356  dssmapnvod  40372  ntrclscls00  40422  rfcnpre3  41296  rfcnpre4  41297  rnmptssbi  41540  infxrgelbrnmpt  41736  xnegre  41748  xrpnf  41768  ioossioobi  41799  iccshift  41800  iocopn  41802  eliccelioc  41803  iooshift  41804  icoopn  41807  qinioo  41817  limcdm0  41905  islptre  41906  islpcn  41926  limcresioolb  41930  climuzlem  42030  climlimsup  42047  liminfgelimsup  42069  liminfgelimsupuz  42075  climliminf  42093  climliminflimsup  42095  climliminflimsup2  42096  xlimpnfxnegmnf  42101  xlimbr  42114  xlimmnfv  42121  xlimpnfv  42125  xlimclim2  42127  dfxlim2v  42134  climresdm  42137  xlimresdm  42146  xlimliminflimsup  42149  fperdvper  42209  itgperiod  42272  fourierdlem32  42431  fourierdlem33  42432  fourierdlem48  42446  fourierdlem49  42447  fourierdlem71  42469  fourierdlem81  42479  preimagelt  42987  preimalegt  42988  smfliminflem  43111  smfliminfmpt  43113  m1mod0mod1  43536  mgmhmf1o  44061  issubmgm2  44064  subsubmgm  44071  resmgmhm2b  44074  rnghmf1o  44181  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  ringcinvALTV  44334