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  5747  funfvbrb  7081  iinpreima  7101  fcdmssb  7154  fnprb  7245  fntpb  7246  fpr2g  7248  nvocnv  7320  fsnex  7322  f1ocnv2d  7706  resf1extb  7980  el2xptp0  8081  1stconst  8148  2ndconst  8149  cnvf1o  8159  fimaproj  8189  tfrlem15  8438  oeeui  8649  ersymb  8770  swoer  8787  erth  8810  boxriin  9006  boxcutc  9007  domunsncan  9134  pw2f1olem  9138  enen1  9174  enen2  9175  domen1  9176  domen2  9177  sdomen1  9178  sdomen2  9179  xpmapenlem  9201  ensymfib  9237  ordiso2  9546  wdomen1  9607  wdomen2  9608  fin23lem26  10442  fpwwe2lem7  10761  r1wunlim  10861  mul2lt0bi  13268  ixxun  13532  xov1plusxeqvd  13669  fzsplit2  13723  fseq1p1m1  13772  elfz2nn0  13792  flflp1  13987  modaddb  14089  modsubdir  14123  zesq  14411  expnngt1b  14427  hashprg  14580  hashgt0elexb  14587  hashbclem  14638  hashge2el2difb  14668  sgn3da  15297  sgnnbi  15300  sgnpbi  15301  sgnmulsgn  15305  rereb  15330  rlimclim  15757  iserex  15868  caucvgb  15891  mptfzshft  15988  fsumrev  15989  climcnds  16064  fprodrev  16188  dvdsadd2b  16520  nn0ob  16598  bitsfzo  16649  dfgcd2  16763  dvdsmulgcd  16774  lcmgcdeq  16831  qden1elz  16977  mrcidb  17839  mrieqvlemd  17853  isacs2  17877  cicer  18031  ssclem  18044  issubc3  18074  ffthiso  18156  fuciso  18203  setcmon  18312  setcepi  18313  setcinv  18315  catciso  18336  acsfiindd  18777  issstrmgm  18881  mgmhmf1o  18939  issubmgm2  18942  subsubmgm  18949  resmgmhm2b  18952  issubmnd  19003  mhmf1o  19041  subsubm  19062  resmhm2b  19068  grpinvid1  19252  grpinvid2  19253  subsubg  19410  ssnmz  19426  qsxpid  19437  ghmf1  19510  kerf1ghm  19511  ghmf1o  19512  conjnmzb  19517  subggim  19530  gicsubgen  19544  ghmqusnsglem1  19545  ghmquskerlem1  19548  ghmqusker  19552  gass  19566  odf1  19827  gex1  19856  fislw  19890  sylow3lem2  19893  sylow3lem6  19897  lsmdisj2a  19952  lsmdisj2b  19953  efgred2  20018  dmdprdsplit  20314  2nsgsimpgd  20369  simpgnsgbid  20370  ablsimpgd  20383  ogrpinv0le  20401  ogrpaddltbi  20404  ogrpaddltrbid  20406  ogrpinv0lt  20408  0unit  20677  irrednegb  20712  rnghmf1o  20733  rhmf1o  20778  subsubrng  20866  subrgunit  20893  subsubrg  20901  rngcinv  20940  ringcinv  20974  isdrng4  21043  isdrng3  21058  issubdrg  21088  islss3  21285  islss4  21288  ellspsn6  21320  lspsneq0b  21339  islmhm2  21364  lmhmf1o  21372  reslmhm2b  21380  lssvs0or  21439  lvecinv  21442  ellspsn4  21453  lspdisjb  21455  islbs2  21483  islbs3  21484  dflidl2rng  21548  drngidl  21590  rngringbd  21655  isprmidlc  21679  prmidl0  21685  qsidom  21689  prmirredlem  21833  islindf3  22187  lindsmm  22189  lsslindf  22191  lsslinds  22192  issubassa  22230  sraassab  22231  issubassa2  22255  gsumbagdiag  22295  subrgasclcl  22431  ply1scleq  22678  matunit  23048  slesolinvbi  23054  en2top  23358  elcls  23446  neindisj2  23496  neiptopnei  23505  neiptopreu  23506  maxlp  23520  neitr  23553  iscncl  23642  cncnp  23653  isreg2  23750  dis2ndc  23834  1stccnp  23836  islly2  23858  dislly  23871  dissnlocfin  23903  kgencmp2  23920  pt1hmeo  24180  xkocnv  24188  t0kq  24192  uffixfr  24297  flimcf  24356  cnpflf2  24374  fclscf  24399  cnextf  24440  utopsnneiplem  24621  isucn2  24652  cfilucfil  24933  psmetutop  24941  restmetu  24944  tngngp2  25026  tngngp  25028  nmoleub  25105  metdseq0  25229  cnheibor  25331  pcophtb  25405  nmoleub2lem  25490  lmmbr  25634  iscfil3  25649  cmetss  25692  cldcss  25817  mbfeqalem2  26018  mbfposb  26029  itg2const2  26117  itgss3  26190  plyco0  26565  dgrlt  26640  ulm2  26769  coseq00topi  26888  coseq0negpitopi  26889  sineq0  26909  relogbcxpb  27172  atans2  27316  xrlimcnp  27353  dchrelbas2  27621  dchrn0  27634  2sqb  27816  nosupbnd2  28130  noinfbnd2  28145  lesrec  28242  ltmuls2  28614  elreno2  28938  istrkg2ld  28979  tgcgreqb  29000  tgbtwncomb  29009  trgcgrg  29035  legov  29105  legov2  29106  legov3  29118  hlbtwn  29134  tglineelsb2  29157  tglinecom  29160  colline  29175  mirinv  29195  mirbtwnb  29201  mirbtwnhl  29209  mirleqb  29223  perpcom  29245  isperp2  29247  oppcom  29277  opphllem3  29282  lnopp2hpgb  29298  colopp  29304  colhp  29305  plngcplem  29320  plngrotlem2  29323  lmieu  29346  iscgra1  29374  dfcgra2  29395  ragsupplcgra  29402  cgraer  29434  angmgmaddeu1  29436  angmgmaddeu2  29437  angmgmaddeu3  29438  angmgmaddeu4  29439  angmgmaddeu5  29440  angmgmaddeu6  29441  angmgmaddeu7  29442  angmgmaddov2lem  29444  angmgmaddcpbl  29447  dfprlng2  29482  edgnbusgreu  30005  nb3grprlem1  30018  lfgriswlk  30328  eleclclwwlknlem2  30709  clwwlknscsh  30710  clwwlknon1  30745  numclwwlk2lem1  31034  grpoinvid1  31187  grpoinvid2  31188  leopmul  32793  hst1h  32886  eqelbid  33170  diffib  33216  ifnebib  33243  iinabrex  33261  disjabrex  33274  disjabrexf  33275  erbr3b  33309  f1o3d  33318  funimass4f  33329  2ndimaxp  33338  fgreu  33363  fcnvgreu  33364  1stpreimas  33396  fcobij  33408  cocnvf1o  33417  resf1o  33418  nn0xmulclb  33459  fzsplit3  33481  fzo0opth  33491  sgnmulsgp  33519  eliccioo  33593  mgcmntco  33654  dfmgc2lem  33655  dfmgc2  33656  pwrssmgc  33660  mgcf1o  33663  mndlrinvb  33685  mndlactfo  33687  mndractfo  33689  mndlactf1o  33690  mndractf1o  33691  gsumhashmul  33727  gsumwrd2dccatlem  33737  cyc3genpm  33812  isarchi3  33847  prmsimpcyc  33888  elrgspnsubrunlem1  33907  elrgspnsubrun  33909  rlocisunit  33936  ricdomn  33950  fracerl  33972  dvdsruasso  34044  dvdsruasso2  34045  dvdsrspss  34046  grplsmid  34059  quslsm  34060  nsgmgc  34067  nsgqusf1olem2  34069  nsgqusf1olem3  34070  pidlnzb  34076  unitpidl1  34078  elrspunidl  34082  elrspunsn  34083  drngidlhash  34087  mxidlirred  34101  mxidlnzrb  34108  qsdrng  34125  dflring3  34133  dflring4  34134  rsprprmprmidlb  34159  rprmirredb  34168  deg1le0eq0  34208  ply1unit  34210  0mplrim  34257  selvply1rhmlem2  34264  evlextv  34285  mplvrpmrhm  34290  esplyfv1  34312  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  lvecdim0  34350  extdg1b  34410  fldextrspunlsp  34417  irngnzply1  34434  1smat1  34547  ist0cld  34576  qtophaus  34579  reff  34582  locfinreflem  34583  cmpcref  34593  zarcls1  34612  zarclsun  34613  zarclsiin  34614  zarclssn  34616  metider  34637  pstmfval  34639  qqhval2  34725  aean  34988  imambfm  35005  eulerpartlemgvv  35119  orvcgteel  35211  orvclteel  35216  ballotlemsf1o  35257  actfunsnf1o  35344  reprsuc  35355  reprpmtf1o  35366  erscottd  35884  sconnpi1  36212  brofs2  37057  brifs2  37058  broutsideof2  37102  ttc0elw  37530  bj-abv  38033  nvo2  38229  irrdiff  38515  ltflcei  38799  poimirlem25  38831  ismblfin  38847  cnambfre  38854  ftc1anclem6  38884  ismndo1  39073  isdrngo2  39158  eqvrelsymb  39888  eqvrelth  39893  lshpnelb  40307  lshpnel2N  40308  lsatspn0  40323  lsatelbN  40329  lsat0cv  40356  lcvexch  40362  lcv1  40364  lkrshp3  40429  lkrpssN  40486  lkrss2N  40492  cvlsupr2  40666  atcvrlln  40843  llncvrlpln  40881  2llnmj  40883  lplncvrlvol  40939  2lplnmj  40945  polcon2bN  41243  pcl0bN  41246  lhpmcvr3  41348  lhpmatb  41354  ltrncoidN  41451  ltrneq3  41531  ltrniotavalbN  41907  cdlemg1cN  41910  diclspsn  42517  dihopelvalcpre  42571  dihord4  42581  dihord  42587  dihmeetlem4preN  42629  dih1dimatlem0  42651  dochsscl  42691  dochoccl  42692  dochord  42693  dochsat  42706  dochshpncl  42707  dochsatshpb  42775  dochshpsat  42777  mapdval4N  42955  mapdsn  42964  hdmap14lem12  43202  hdmapip0  43238  hlhillcs  43281  resuppsinopn  43680  mulgt0b2d  43808  mullt0b1d  43813  mullt0b2d  43814  riccrng  43849  ricdrng  43859  prjspnnorm  43927  mrefg2  43984  mzpmfp  44024  lzenom  44047  elpell14qr2  44135  elpell1qr2  44145  pellfund14b  44172  congabseq  44247  acongeq  44256  jm2.23  44269  jm2.20nn  44270  jm2.25lem1  44271  wepwsolem  44315  islssfg2  44339  lnmlmic  44356  dfacbasgrp  44375  unielss  44481  rfovcnvf1od  45265  dssmapnvod  45281  ntrclscls00  45327  rfcnpre3  46324  rfcnpre4  46325  ssmapsn  46502  rnmptssbi  46545  infxrgelbrnmpt  46737  xnegre  46749  xrpnf  46768  rexanuz2nf  46775  ioossioobi  46802  iccshift  46803  iocopn  46805  eliccelioc  46806  iooshift  46807  icoopn  46810  qinioo  46820  limcdm0  46903  islptre  46904  islpcn  46922  limcresioolb  46926  climuzlem  47026  climlimsup  47043  liminfgelimsup  47065  liminfgelimsupuz  47071  climliminf  47089  climliminflimsup  47091  climliminflimsup2  47092  xlimpnfxnegmnf  47097  xlimbr  47110  xlimmnfv  47117  xlimpnfv  47121  xlimclim2  47123  dfxlim2v  47130  climresdm  47133  xlimresdm  47142  xlimliminflimsup  47145  fperdvper  47202  itgperiod  47264  fourierdlem32  47422  fourierdlem33  47423  fourierdlem48  47437  fourierdlem49  47438  fourierdlem71  47460  fourierdlem81  47470  preimagelt  47982  preimalegt  47983  smfliminflem  48113  smfliminfmpt  48115  chnsubseqwl  48162  fcoresfob  48415  m1mod0mod1  48703  uhgrimedg  49262  isubgr3stgrlem8  49344  rngcinvALTV  49646  ringcinvALTV  49680  prelrrx2bd  50157  xpco2  50299  ovconstbrd  50304  ovconstbrn0d  50305  lubeldm2  50401  glbeldm2  50402  upeu2lem  50473  sectpropd  50482  invpropd  50484  isopropd  50486  cicerALT  50491  cicpropd  50495  up1st2ndb  50634  uobffth  50665  uobeqw  50666  natoppfb  50684  oppc1stflem  50740  fucofulem1  50763  functhinclem1  50910  fullthinc  50916  thincciso4  50923  thinciso  50936  functermclem  50973  termcterm3  50981  termcciso  50982  termcarweu  50994  termfucterm  51013  prstchom2ALT  51033  lanval2  51141  ranval2  51144