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  5739  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  33071  diffib  33117  ifnebib  33145  iinabrex  33163  disjabrex  33176  disjabrexf  33177  erbr3b  33211  f1o3d  33220  funimass4f  33231  2ndimaxp  33240  fgreu  33265  fcnvgreu  33266  1stpreimas  33299  fcobij  33312  cocnvf1o  33321  resf1o  33322  nn0xmulclb  33363  fzsplit3  33385  fzo0opth  33395  sgnmulsgp  33423  eliccioo  33497  mgcmntco  33555  dfmgc2lem  33556  dfmgc2  33557  pwrssmgc  33561  mgcf1o  33564  mndlrinvb  33586  mndlactfo  33588  mndractfo  33590  mndlactf1o  33591  mndractf1o  33592  gsumhashmul  33628  gsumwrd2dccatlem  33638  cyc3genpm  33713  isarchi3  33748  prmsimpcyc  33789  elrgspnsubrunlem1  33808  elrgspnsubrun  33810  rlocisunit  33837  ricdomn  33851  fracerl  33868  dvdsruasso  33940  dvdsruasso2  33941  dvdsrspss  33942  grplsmid  33955  quslsm  33956  nsgmgc  33963  nsgqusf1olem2  33965  nsgqusf1olem3  33966  pidlnzb  33972  unitpidl1  33974  elrspunidl  33978  elrspunsn  33979  drngidlhash  33983  mxidlirred  33997  mxidlnzrb  34004  qsdrng  34021  dflring3  34029  dflring4  34030  rsprprmprmidlb  34055  rprmirredb  34064  deg1le0eq0  34105  ply1unit  34107  0mplrim  34146  selvply1rhmlem2  34153  evlextv  34174  mplvrpmrhm  34179  esplyfv1  34201  esplyfval1  34205  esplyfvaln  34206  esplyind  34207  lvecdim0  34239  extdg1b  34299  fldextrspunlsp  34306  irngnzply1  34323  1smat1  34436  ist0cld  34465  qtophaus  34468  reff  34471  locfinreflem  34472  cmpcref  34482  zarcls1  34501  zarclsun  34502  zarclsiin  34503  zarclssn  34505  metider  34526  pstmfval  34528  qqhval2  34614  aean  34877  imambfm  34894  eulerpartlemgvv  35008  orvcgteel  35100  orvclteel  35105  ballotlemsf1o  35146  actfunsnf1o  35233  reprsuc  35244  reprpmtf1o  35255  sconnpi1  36004  brofs2  36842  brifs2  36843  broutsideof2  36887  ttc0elw  37315  bj-abv  37818  irrdiff  38247  ltflcei  38531  poimirlem25  38563  ismblfin  38579  cnambfre  38586  ftc1anclem6  38616  ismndo1  38807  isdrngo2  38892  eqvrelsymb  39622  eqvrelth  39627  lshpnelb  40041  lshpnel2N  40042  lsatspn0  40057  lsatelbN  40063  lsat0cv  40090  lcvexch  40096  lcv1  40098  lkrshp3  40163  lkrpssN  40220  lkrss2N  40226  cvlsupr2  40400  atcvrlln  40577  llncvrlpln  40615  2llnmj  40617  lplncvrlvol  40673  2lplnmj  40679  polcon2bN  40977  pcl0bN  40980  lhpmcvr3  41082  lhpmatb  41088  ltrncoidN  41185  ltrneq3  41265  ltrniotavalbN  41641  cdlemg1cN  41644  diclspsn  42251  dihopelvalcpre  42305  dihord4  42315  dihord  42321  dihmeetlem4preN  42363  dih1dimatlem0  42385  dochsscl  42425  dochoccl  42426  dochord  42427  dochsat  42440  dochshpncl  42441  dochsatshpb  42509  dochshpsat  42511  mapdval4N  42689  mapdsn  42698  hdmap14lem12  42936  hdmapip0  42972  hlhillcs  43015  resuppsinopn  43414  mulgt0b2d  43542  mullt0b1d  43547  mullt0b2d  43548  riccrng  43583  ricdrng  43593  prjspnnorm  43661  mrefg2  43717  mzpmfp  43757  lzenom  43780  elpell14qr2  43868  elpell1qr2  43878  pellfund14b  43905  congabseq  43980  acongeq  43989  jm2.23  44002  jm2.20nn  44003  jm2.25lem1  44004  wepwsolem  44048  islssfg2  44072  lnmlmic  44089  dfacbasgrp  44109  unielss  44219  rfovcnvf1od  45003  dssmapnvod  45019  ntrclscls00  45065  rfcnpre3  46049  rfcnpre4  46050  ssmapsn  46228  rnmptssbi  46271  infxrgelbrnmpt  46463  xnegre  46475  xrpnf  46494  rexanuz2nf  46501  ioossioobi  46528  iccshift  46529  iocopn  46531  eliccelioc  46532  iooshift  46533  icoopn  46536  qinioo  46546  limcdm0  46629  islptre  46630  islpcn  46648  limcresioolb  46652  climuzlem  46752  climlimsup  46769  liminfgelimsup  46791  liminfgelimsupuz  46797  climliminf  46815  climliminflimsup  46817  climliminflimsup2  46818  xlimpnfxnegmnf  46823  xlimbr  46836  xlimmnfv  46843  xlimpnfv  46847  xlimclim2  46849  dfxlim2v  46856  climresdm  46859  xlimresdm  46868  xlimliminflimsup  46871  fperdvper  46928  itgperiod  46990  fourierdlem32  47148  fourierdlem33  47149  fourierdlem48  47163  fourierdlem49  47164  fourierdlem71  47186  fourierdlem81  47196  preimagelt  47708  preimalegt  47709  smfliminflem  47839  smfliminfmpt  47841  chnsubseqwl  47888  fcoresfob  48141  m1mod0mod1  48429  uhgrimedg  48988  isubgr3stgrlem8  49070  rngcinvALTV  49372  ringcinvALTV  49406  xpco2  49966  ovconstbrd  49971  ovconstbrn0d  49972  lubeldm2  50063  glbeldm2  50064  upeu2lem  50135  sectpropd  50144  invpropd  50146  isopropd  50148  cicerALT  50153  cicpropd  50157  up1st2ndb  50294  uobffth  50325  uobeqw  50326  natoppfb  50338  oppc1stflem  50394  fucofulem1  50417  functhinclem1  50551  fullthinc  50557  thincciso4  50564  thinciso  50577  functermclem  50614  termcterm3  50622  termcciso  50623  termcarweu  50635  termfucterm  50651  prstchom2ALT  50671  lanval2  50734  ranval2  50737