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  bibiad  839  eqrdav  2728  eqsndOLD  4791  frsn  5719  funfvbrb  7005  iinpreima  7023  fcdmssb  7076  fnprb  7164  fntpb  7165  fpr2g  7167  nvocnv  7238  fsnex  7240  f1ocnv2d  7622  resf1extb  7890  el2xptp0  7994  1stconst  8056  2ndconst  8057  cnvf1o  8067  fimaproj  8091  tfrlem15  8337  oeeui  8543  ersymb  8662  swoer  8679  erth  8702  boxriin  8890  boxcutc  8891  domunsncan  9018  pw2f1olem  9022  enen1  9058  enen2  9059  domen1  9060  domen2  9061  sdomen1  9062  sdomen2  9063  xpmapenlem  9085  ensymfib  9125  ordiso2  9444  wdomen1  9505  wdomen2  9506  fin23lem26  10254  fpwwe2lem7  10566  r1wunlim  10666  mul2lt0bi  13035  ixxun  13298  xov1plusxeqvd  13435  fzsplit2  13486  fseq1p1m1  13535  elfz2nn0  13555  flflp1  13745  modaddb  13847  modsubdir  13881  zesq  14167  expnngt1b  14183  hashprg  14336  hashgt0elexb  14343  hashbclem  14393  hashge2el2difb  14423  rereb  15062  rlimclim  15488  iserex  15599  caucvgb  15622  mptfzshft  15720  fsumrev  15721  climcnds  15793  fprodrev  15919  dvdsadd2b  16252  nn0ob  16330  bitsfzo  16381  dfgcd2  16492  dvdsmulgcd  16502  lcmgcdeq  16558  qden1elz  16703  mrcidb  17556  mrieqvlemd  17570  isacs2  17594  cicer  17748  ssclem  17761  issubc3  17791  ffthiso  17873  fuciso  17920  setcmon  18029  setcepi  18030  setcinv  18032  catciso  18053  acsfiindd  18494  issstrmgm  18562  mgmhmf1o  18609  issubmgm2  18612  subsubmgm  18619  resmgmhm2b  18622  issubmnd  18670  mhmf1o  18705  subsubm  18725  resmhm2b  18731  grpinvid1  18905  grpinvid2  18906  subsubg  19063  ssnmz  19080  ghmf1  19160  kerf1ghm  19161  ghmf1o  19162  conjnmzb  19167  subggim  19180  gicsubgen  19193  ghmqusnsglem1  19194  ghmquskerlem1  19197  ghmqusker  19201  gass  19215  odf1  19476  gex1  19505  fislw  19539  sylow3lem2  19542  sylow3lem6  19546  lsmdisj2a  19601  lsmdisj2b  19602  efgred2  19667  dmdprdsplit  19963  2nsgsimpgd  20018  simpgnsgbid  20019  ablsimpgd  20032  ogrpinv0le  20050  ogrpaddltbi  20053  ogrpaddltrbid  20055  ogrpinv0lt  20057  0unit  20316  irrednegb  20351  rnghmf1o  20372  rhmf1o  20411  subsubrng  20483  subrgunit  20510  subsubrg  20518  rngcinv  20557  ringcinv  20591  isdrng2  20663  issubdrg  20700  islss3  20897  islss4  20900  ellspsn6  20932  lspsneq0b  20951  islmhm2  20977  lmhmf1o  20985  reslmhm2b  20993  lssvs0or  21052  lvecinv  21055  ellspsn4  21066  lspdisjb  21068  islbs2  21096  islbs3  21097  dflidl2rng  21160  rngringbd  21250  prmirredlem  21414  islindf3  21768  lindsmm  21770  lsslindf  21772  lsslinds  21773  issubassa  21809  sraassab  21810  issubassa2  21834  gsumbagdiag  21873  subrgasclcl  22007  ply1scleq  22225  matunit  22598  slesolinvbi  22601  en2top  22905  elcls  22993  neindisj2  23043  neiptopnei  23052  neiptopreu  23053  maxlp  23067  neitr  23100  iscncl  23189  cncnp  23200  isreg2  23297  dis2ndc  23380  1stccnp  23382  islly2  23404  dislly  23417  dissnlocfin  23449  kgencmp2  23466  pt1hmeo  23726  xkocnv  23734  t0kq  23738  uffixfr  23843  flimcf  23902  cnpflf2  23920  fclscf  23945  cnextf  23986  utopsnneiplem  24168  isucn2  24199  cfilucfil  24480  psmetutop  24488  restmetu  24491  tngngp2  24573  tngngp  24575  nmoleub  24652  metdseq0  24776  cnheibor  24887  pcophtb  24962  nmoleub2lem  25047  lmmbr  25191  iscfil3  25206  cmetss  25249  cldcss  25374  mbfeqalem2  25576  mbfposb  25587  itg2const2  25675  itgss3  25749  plyco0  26130  dgrlt  26205  ulm2  26327  coseq00topi  26444  coseq0negpitopi  26445  sineq0  26466  relogbcxpb  26730  atans2  26874  xrlimcnp  26911  dchrelbas2  27181  dchrn0  27194  2sqb  27376  nosupbnd2  27661  noinfbnd2  27676  slerec  27765  sltmul2  28114  istrkg2ld  28440  tgcgreqb  28461  tgbtwncomb  28469  trgcgrg  28495  legov  28565  legov2  28566  legov3  28578  hlbtwn  28591  tglineelsb2  28612  tglinecom  28615  colline  28629  mirinv  28646  mirbtwnb  28652  mirbtwnhl  28660  perpcom  28693  isperp2  28695  oppcom  28724  opphllem3  28729  lnopp2hpgb  28743  colopp  28749  colhp  28750  lmieu  28764  iscgra1  28790  dfcgra2  28810  edgnbusgreu  29347  nb3grprlem1  29360  lfgriswlk  29667  eleclclwwlknlem2  30040  clwwlknscsh  30041  clwwlknon1  30076  numclwwlk2lem1  30355  grpoinvid1  30507  grpoinvid2  30508  leopmul  32113  hst1h  32206  eqelbid  32454  diffib  32500  ifnebib  32528  iinabrex  32548  disjabrex  32561  disjabrexf  32562  erbr3b  32595  f1o3d  32601  funimass4f  32611  2ndimaxp  32620  fgreu  32646  fcnvgreu  32647  1stpreimas  32679  fcobij  32695  resf1o  32703  nn0xmulclb  32744  fzsplit3  32766  fzo0opth  32778  sgn3da  32809  sgnnbi  32813  sgnpbi  32814  sgnmulsgn  32817  sgnmulsgp  32818  eliccioo  32901  mgcmntco  32966  dfmgc2lem  32967  dfmgc2  32968  pwrssmgc  32972  mgcf1o  32975  mndlrinvb  33009  mndlactfo  33011  mndractfo  33013  mndlactf1o  33014  mndractf1o  33015  gsumhashmul  33044  gsumwrd2dccatlem  33049  cyc3genpm  33124  isarchi3  33156  prmsimpcyc  33197  elrgspnsubrunlem1  33214  elrgspnsubrun  33216  domnlcanbOLD  33247  isdrng4  33261  fracerl  33272  qsxpid  33326  dvdsruasso  33349  dvdsruasso2  33350  dvdsrspss  33351  grplsmid  33368  quslsm  33369  nsgmgc  33376  nsgqusf1olem2  33378  nsgqusf1olem3  33379  pidlnzb  33386  unitpidl1  33388  elrspunidl  33392  elrspunsn  33393  drngidl  33397  drngidlhash  33398  isprmidlc  33411  prmidl0  33414  qsidom  33418  mxidlirred  33436  mxidlnzrb  33444  qsdrng  33461  rsprprmprmidlb  33487  rprmirredb  33496  deg1le0eq0  33535  ply1unit  33537  lvecdim0  33595  extdg1b  33655  fldextrspunlsp  33662  irngnzply1  33679  1smat1  33787  ist0cld  33816  qtophaus  33819  reff  33822  locfinreflem  33823  cmpcref  33833  zarcls1  33852  zarclsun  33853  zarclsiin  33854  zarclssn  33856  metider  33877  pstmfval  33879  qqhval2  33965  aean  34227  imambfm  34246  eulerpartlemgvv  34360  orvcgteel  34452  orvclteel  34457  ballotlemsf1o  34498  actfunsnf1o  34588  reprsuc  34599  reprpmtf1o  34610  sconnpi1  35219  brofs2  36058  brifs2  36059  broutsideof2  36103  bj-abv  36887  irrdiff  37307  ltflcei  37595  poimirlem25  37632  ismblfin  37648  cnambfre  37655  ftc1anclem6  37685  ismndo1  37860  isdrngo2  37945  eqvrelsymb  38590  eqvrelth  38595  lshpnelb  38970  lshpnel2N  38971  lsatspn0  38986  lsatelbN  38992  lsat0cv  39019  lcvexch  39025  lcv1  39027  lkrshp3  39092  lkrpssN  39149  lkrss2N  39155  cvlsupr2  39329  atcvrlln  39507  llncvrlpln  39545  2llnmj  39547  lplncvrlvol  39603  2lplnmj  39609  polcon2bN  39907  pcl0bN  39910  lhpmcvr3  40012  lhpmatb  40018  ltrncoidN  40115  ltrneq3  40195  ltrniotavalbN  40571  cdlemg1cN  40574  diclspsn  41181  dihopelvalcpre  41235  dihord4  41245  dihord  41251  dihmeetlem4preN  41293  dih1dimatlem0  41315  dochsscl  41355  dochoccl  41356  dochord  41357  dochsat  41370  dochshpncl  41371  dochsatshpb  41439  dochshpsat  41441  mapdval4N  41619  mapdsn  41628  hdmap14lem12  41866  hdmapip0  41902  hlhillcs  41945  resuppsinopn  42344  mulgt0b2d  42459  mullt0b1d  42464  mullt0b2d  42465  riccrng  42503  ricdrng  42510  prjspner1  42607  mrefg2  42688  mzpmfp  42728  lzenom  42751  elpell14qr2  42843  elpell1qr2  42853  pellfund14b  42880  congabseq  42956  acongeq  42965  jm2.23  42978  jm2.20nn  42979  jm2.25lem1  42980  wepwsolem  43024  islssfg2  43053  lnmlmic  43070  dfacbasgrp  43090  unielss  43200  rfovcnvf1od  43986  dssmapnvod  44002  ntrclscls00  44048  rfcnpre3  45020  rfcnpre4  45021  ssmapsn  45203  rnmptssbi  45247  infxrgelbrnmpt  45443  xnegre  45455  xrpnf  45474  rexanuz2nf  45481  ioossioobi  45508  iccshift  45509  iocopn  45511  eliccelioc  45512  iooshift  45513  icoopn  45516  qinioo  45526  limcdm0  45609  islptre  45610  islpcn  45630  limcresioolb  45634  climuzlem  45734  climlimsup  45751  liminfgelimsup  45773  liminfgelimsupuz  45779  climliminf  45797  climliminflimsup  45799  climliminflimsup2  45800  xlimpnfxnegmnf  45805  xlimbr  45818  xlimmnfv  45825  xlimpnfv  45829  xlimclim2  45831  dfxlim2v  45838  climresdm  45841  xlimresdm  45850  xlimliminflimsup  45853  fperdvper  45910  itgperiod  45972  fourierdlem32  46130  fourierdlem33  46131  fourierdlem48  46145  fourierdlem49  46146  fourierdlem71  46168  fourierdlem81  46178  preimagelt  46690  preimalegt  46691  smfliminflem  46821  smfliminfmpt  46823  fcoresfob  47066  m1mod0mod1  47348  uhgrimedg  47884  isubgr3stgrlem8  47965  rngcinvALTV  48257  ringcinvALTV  48291  xpco2  48838  fvconstr  48843  fvconstrn0  48844  lubeldm2  48937  glbeldm2  48938  upeu2lem  49010  sectpropd  49019  invpropd  49021  isopropd  49023  cicerALT  49028  cicpropd  49032  up1st2ndb  49169  uobffth  49200  uobeqw  49201  natoppfb  49213  oppc1stflem  49269  fucofulem1  49292  functhinclem1  49426  fullthinc  49432  thincciso4  49439  thinciso  49452  functermclem  49489  termcterm3  49497  termcciso  49498  termcarweu  49510  termfucterm  49526  prstchom2ALT  49546  lanval2  49609  ranval2  49612