Theorem impbida 813

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biadanid  835  bibiad  853  frsn  5738  funfvbrb  7050  iinpreima  7069  fcdmssb  7122  fnprb  7214  fntpb  7215  fpr2g  7217  nvocnv  7289  fsnex  7291  f1ocnv2d  7674  resf1extb  7946  el2xptp0  8047  1stconst  8111  2ndconst  8112  cnvf1o  8122  fimaproj  8152  tfrlem15  8400  oeeui  8611  ersymb  8732  swoer  8749  erth  8772  boxriin  8968  boxcutc  8969  domunsncan  9096  pw2f1olem  9100  enen1  9136  enen2  9137  domen1  9138  domen2  9139  sdomen1  9140  sdomen2  9141  xpmapenlem  9163  ensymfib  9199  ordiso2  9509  wdomen1  9570  wdomen2  9571  fin23lem26  10403  fpwwe2lem7  10722  r1wunlim  10822  mul2lt0bi  13228  ixxun  13492  xov1plusxeqvd  13629  fzsplit2  13683  fseq1p1m1  13732  elfz2nn0  13752  flflp1  13947  modaddb  14049  modsubdir  14083  zesq  14370  expnngt1b  14386  hashprg  14539  hashgt0elexb  14546  hashbclem  14597  hashge2el2difb  14627  sgn3da  15254  sgnnbi  15257  sgnpbi  15258  sgnmulsgn  15262  rereb  15287  rlimclim  15713  iserex  15824  caucvgb  15847  mptfzshft  15944  fsumrev  15945  climcnds  16020  fprodrev  16144  dvdsadd2b  16476  nn0ob  16554  bitsfzo  16605  dfgcd2  16719  dvdsmulgcd  16730  lcmgcdeq  16787  qden1elz  16933  mrcidb  17789  mrieqvlemd  17803  isacs2  17827  cicer  17981  ssclem  17994  issubc3  18024  ffthiso  18106  fuciso  18153  setcmon  18262  setcepi  18263  setcinv  18265  catciso  18286  acsfiindd  18727  issstrmgm  18831  mgmhmf1o  18889  issubmgm2  18892  subsubmgm  18899  resmgmhm2b  18902  issubmnd  18953  mhmf1o  18991  subsubm  19012  resmhm2b  19018  grpinvid1  19202  grpinvid2  19203  subsubg  19360  ssnmz  19376  qsxpid  19387  ghmf1  19460  kerf1ghm  19461  ghmf1o  19462  conjnmzb  19467  subggim  19480  gicsubgen  19493  ghmqusnsglem1  19494  ghmquskerlem1  19497  ghmqusker  19501  gass  19515  odf1  19776  gex1  19805  fislw  19839  sylow3lem2  19842  sylow3lem6  19846  lsmdisj2a  19901  lsmdisj2b  19902  efgred2  19967  dmdprdsplit  20263  2nsgsimpgd  20318  simpgnsgbid  20319  ablsimpgd  20332  ogrpinv0le  20350  ogrpaddltbi  20353  ogrpaddltrbid  20355  ogrpinv0lt  20357  0unit  20626  irrednegb  20661  rnghmf1o  20682  rhmf1o  20727  subsubrng  20815  subrgunit  20842  subsubrg  20850  rngcinv  20889  ringcinv  20923  isdrng4  20992  isdrng3  21007  issubdrg  21037  islss3  21234  islss4  21237  ellspsn6  21269  lspsneq0b  21288  islmhm2  21313  lmhmf1o  21321  reslmhm2b  21329  lssvs0or  21388  lvecinv  21391  ellspsn4  21402  lspdisjb  21404  islbs2  21432  islbs3  21433  dflidl2rng  21497  drngidl  21539  rngringbd  21604  isprmidlc  21628  prmidl0  21634  qsidom  21638  prmirredlem  21778  islindf3  22132  lindsmm  22134  lsslindf  22136  lsslinds  22137  issubassa  22175  sraassab  22176  issubassa2  22200  gsumbagdiag  22240  subrgasclcl  22376  ply1scleq  22623  matunit  22993  slesolinvbi  22999  en2top  23303  elcls  23391  neindisj2  23441  neiptopnei  23450  neiptopreu  23451  maxlp  23465  neitr  23498  iscncl  23587  cncnp  23598  isreg2  23695  dis2ndc  23779  1stccnp  23781  islly2  23803  dislly  23816  dissnlocfin  23848  kgencmp2  23865  pt1hmeo  24125  xkocnv  24133  t0kq  24137  uffixfr  24242  flimcf  24301  cnpflf2  24319  fclscf  24344  cnextf  24385  utopsnneiplem  24566  isucn2  24597  cfilucfil  24878  psmetutop  24886  restmetu  24889  tngngp2  24971  tngngp  24973  nmoleub  25050  metdseq0  25174  cnheibor  25276  pcophtb  25350  nmoleub2lem  25435  lmmbr  25579  iscfil3  25594  cmetss  25637  cldcss  25762  mbfeqalem2  25963  mbfposb  25974  itg2const2  26062  itgss3  26135  plyco0  26510  dgrlt  26585  ulm2  26712  coseq00topi  26831  coseq0negpitopi  26832  sineq0  26852  relogbcxpb  27115  atans2  27259  xrlimcnp  27296  dchrelbas2  27564  dchrn0  27577  2sqb  27759  nosupbnd2  28073  noinfbnd2  28088  lesrec  28185  ltmuls2  28557  elreno2  28881  istrkg2ld  28922  tgcgreqb  28943  tgbtwncomb  28952  trgcgrg  28978  legov  29048  legov2  29049  legov3  29061  hlbtwn  29077  tglineelsb2  29100  tglinecom  29103  colline  29118  mirinv  29138  mirbtwnb  29144  mirbtwnhl  29152  mirleqb  29166  perpcom  29188  isperp2  29190  oppcom  29220  opphllem3  29225  lnopp2hpgb  29241  colopp  29247  colhp  29248  plngcplem  29263  plngrotlem2  29266  lmieu  29289  iscgra1  29317  dfcgra2  29338  ragsupplcgra  29345  cgraer  29377  angmgmaddeu1  29379  angmgmaddeu2  29380  angmgmaddeu3  29381  angmgmaddeu4  29382  angmgmaddeu5  29383  angmgmaddeu6  29384  angmgmaddeu7  29385  angmgmaddov2lem  29387  angmgmaddcpbl  29390  dfprlng2  29425  edgnbusgreu  29948  nb3grprlem1  29961  lfgriswlk  30271  eleclclwwlknlem2  30652  clwwlknscsh  30653  clwwlknon1  30688  numclwwlk2lem1  30977  grpoinvid1  31130  grpoinvid2  31131  leopmul  32736  hst1h  32829  eqelbid  33113  diffib  33159  ifnebib  33187  iinabrex  33205  disjabrex  33218  disjabrexf  33219  erbr3b  33253  f1o3d  33262  funimass4f  33273  2ndimaxp  33282  fgreu  33307  fcnvgreu  33308  1stpreimas  33341  fcobij  33354  cocnvf1o  33363  resf1o  33364  nn0xmulclb  33405  fzsplit3  33427  fzo0opth  33437  sgnmulsgp  33465  eliccioo  33539  mgcmntco  33597  dfmgc2lem  33598  dfmgc2  33599  pwrssmgc  33603  mgcf1o  33606  mndlrinvb  33628  mndlactfo  33630  mndractfo  33632  mndlactf1o  33633  mndractf1o  33634  gsumhashmul  33670  gsumwrd2dccatlem  33680  cyc3genpm  33755  isarchi3  33790  prmsimpcyc  33831  elrgspnsubrunlem1  33850  elrgspnsubrun  33852  rlocisunit  33879  ricdomn  33893  fracerl  33910  dvdsruasso  33982  dvdsruasso2  33983  dvdsrspss  33984  grplsmid  33997  quslsm  33998  nsgmgc  34005  nsgqusf1olem2  34007  nsgqusf1olem3  34008  pidlnzb  34014  unitpidl1  34016  elrspunidl  34020  elrspunsn  34021  drngidlhash  34025  mxidlirred  34039  mxidlnzrb  34046  qsdrng  34063  dflring3  34071  dflring4  34072  rsprprmprmidlb  34097  rprmirredb  34106  deg1le0eq0  34147  ply1unit  34149  0mplrim  34188  selvply1rhmlem2  34195  evlextv  34216  mplvrpmrhm  34221  esplyfv1  34243  esplyfval1  34247  esplyfvaln  34248  esplyind  34249  lvecdim0  34281  extdg1b  34341  fldextrspunlsp  34348  irngnzply1  34365  1smat1  34478  ist0cld  34507  qtophaus  34510  reff  34513  locfinreflem  34514  cmpcref  34524  zarcls1  34543  zarclsun  34544  zarclsiin  34545  zarclssn  34547  metider  34568  pstmfval  34570  qqhval2  34656  aean  34919  imambfm  34936  eulerpartlemgvv  35050  orvcgteel  35142  orvclteel  35147  ballotlemsf1o  35188  actfunsnf1o  35275  reprsuc  35286  reprpmtf1o  35297  sconnpi1  36046  brofs2  36884  brifs2  36885  broutsideof2  36929  ttc0elw  37357  bj-abv  37860  irrdiff  38290  ltflcei  38574  poimirlem25  38606  ismblfin  38622  cnambfre  38629  ftc1anclem6  38659  ismndo1  38850  isdrngo2  38935  eqvrelsymb  39665  eqvrelth  39670  lshpnelb  40084  lshpnel2N  40085  lsatspn0  40100  lsatelbN  40106  lsat0cv  40133  lcvexch  40139  lcv1  40141  lkrshp3  40206  lkrpssN  40263  lkrss2N  40269  cvlsupr2  40443  atcvrlln  40620  llncvrlpln  40658  2llnmj  40660  lplncvrlvol  40716  2lplnmj  40722  polcon2bN  41020  pcl0bN  41023  lhpmcvr3  41125  lhpmatb  41131  ltrncoidN  41228  ltrneq3  41308  ltrniotavalbN  41684  cdlemg1cN  41687  diclspsn  42294  dihopelvalcpre  42348  dihord4  42358  dihord  42364  dihmeetlem4preN  42406  dih1dimatlem0  42428  dochsscl  42468  dochoccl  42469  dochord  42470  dochsat  42483  dochshpncl  42484  dochsatshpb  42552  dochshpsat  42554  mapdval4N  42732  mapdsn  42741  hdmap14lem12  42979  hdmapip0  43015  hlhillcs  43058  resuppsinopn  43457  mulgt0b2d  43585  mullt0b1d  43590  mullt0b2d  43591  riccrng  43626  ricdrng  43636  prjspnnorm  43704  mrefg2  43760  mzpmfp  43800  lzenom  43823  elpell14qr2  43911  elpell1qr2  43921  pellfund14b  43948  congabseq  44023  acongeq  44032  jm2.23  44045  jm2.20nn  44046  jm2.25lem1  44047  wepwsolem  44091  islssfg2  44115  lnmlmic  44132  dfacbasgrp  44152  unielss  44262  rfovcnvf1od  45046  dssmapnvod  45062  ntrclscls00  45108  rfcnpre3  46092  rfcnpre4  46093  ssmapsn  46271  rnmptssbi  46314  infxrgelbrnmpt  46506  xnegre  46518  xrpnf  46537  rexanuz2nf  46544  ioossioobi  46571  iccshift  46572  iocopn  46574  eliccelioc  46575  iooshift  46576  icoopn  46579  qinioo  46589  limcdm0  46672  islptre  46673  islpcn  46691  limcresioolb  46695  climuzlem  46795  climlimsup  46812  liminfgelimsup  46834  liminfgelimsupuz  46840  climliminf  46858  climliminflimsup  46860  climliminflimsup2  46861  xlimpnfxnegmnf  46866  xlimbr  46879  xlimmnfv  46886  xlimpnfv  46890  xlimclim2  46892  dfxlim2v  46899  climresdm  46902  xlimresdm  46911  xlimliminflimsup  46914  fperdvper  46971  itgperiod  47033  fourierdlem32  47191  fourierdlem33  47192  fourierdlem48  47206  fourierdlem49  47207  fourierdlem71  47229  fourierdlem81  47239  preimagelt  47751  preimalegt  47752  smfliminflem  47882  smfliminfmpt  47884  chnsubseqwl  47931  fcoresfob  48184  m1mod0mod1  48472  uhgrimedg  49031  isubgr3stgrlem8  49113  rngcinvALTV  49415  ringcinvALTV  49449  xpco2  50009  ovconstbrd  50014  ovconstbrn0d  50015  lubeldm2  50106  glbeldm2  50107  upeu2lem  50178  sectpropd  50187  invpropd  50189  isopropd  50191  cicerALT  50196  cicpropd  50200  up1st2ndb  50337  uobffth  50368  uobeqw  50369  natoppfb  50381  oppc1stflem  50437  fucofulem1  50460  functhinclem1  50594  fullthinc  50600  thincciso4  50607  thinciso  50620  functermclem  50657  termcterm3  50665  termcciso  50666  termcarweu  50678  termfucterm  50694  prstchom2ALT  50714  lanval2  50777  ranval2  50780