Theorem impbida 812

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 417	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 417	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 215	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biadanid  834  bibiad  852  frsn  5750  funfvbrb  7047  iinpreima  7065  fcdmssb  7118  fnprb  7207  fntpb  7208  fpr2g  7210  nvocnv  7280  fsnex  7282  f1ocnv2d  7664  resf1extb  7931  el2xptp0  8033  1stconst  8095  2ndconst  8096  cnvf1o  8106  fimaproj  8131  tfrlem15  8379  oeeui  8588  ersymb  8709  swoer  8726  erth  8749  boxriin  8938  boxcutc  8939  domunsncan  9065  pw2f1olem  9069  enen1  9105  enen2  9106  domen1  9107  domen2  9108  sdomen1  9109  sdomen2  9110  xpmapenlem  9132  ensymfib  9168  ordiso2  9477  wdomen1  9538  wdomen2  9539  fin23lem26  10309  fpwwe2lem7  10622  r1wunlim  10722  mul2lt0bi  13124  ixxun  13388  xov1plusxeqvd  13525  fzsplit2  13577  fseq1p1m1  13626  elfz2nn0  13646  flflp1  13840  modaddb  13942  modsubdir  13976  zesq  14262  expnngt1b  14278  hashprg  14431  hashgt0elexb  14438  hashbclem  14489  hashge2el2difb  14519  sgn3da  15138  sgnnbi  15141  sgnpbi  15142  sgnmulsgn  15146  rereb  15171  rlimclim  15597  iserex  15708  caucvgb  15731  mptfzshft  15829  fsumrev  15830  climcnds  15905  fprodrev  16031  dvdsadd2b  16364  nn0ob  16442  bitsfzo  16493  dfgcd2  16604  dvdsmulgcd  16614  lcmgcdeq  16670  qden1elz  16816  mrcidb  17671  mrieqvlemd  17685  isacs2  17709  cicer  17863  ssclem  17876  issubc3  17906  ffthiso  17988  fuciso  18035  setcmon  18144  setcepi  18145  setcinv  18147  catciso  18168  acsfiindd  18609  issstrmgm  18711  mgmhmf1o  18758  issubmgm2  18761  subsubmgm  18768  resmgmhm2b  18771  issubmnd  18819  mhmf1o  18854  subsubm  18875  resmhm2b  18881  grpinvid1  19058  grpinvid2  19059  subsubg  19216  ssnmz  19232  qsxpid  19243  ghmf1  19316  kerf1ghm  19317  ghmf1o  19318  conjnmzb  19323  subggim  19336  gicsubgen  19349  ghmqusnsglem1  19350  ghmquskerlem1  19353  ghmqusker  19357  gass  19371  odf1  19632  gex1  19661  fislw  19695  sylow3lem2  19698  sylow3lem6  19702  lsmdisj2a  19757  lsmdisj2b  19758  efgred2  19823  dmdprdsplit  20119  2nsgsimpgd  20174  simpgnsgbid  20175  ablsimpgd  20188  ogrpinv0le  20206  ogrpaddltbi  20209  ogrpaddltrbid  20211  ogrpinv0lt  20213  0unit  20478  irrednegb  20513  rnghmf1o  20534  rhmf1o  20573  subsubrng  20648  subrgunit  20675  subsubrg  20683  rngcinv  20722  ringcinv  20756  isdrng2  20827  issubdrg  20861  islss3  21058  islss4  21061  ellspsn6  21093  lspsneq0b  21112  islmhm2  21137  lmhmf1o  21145  reslmhm2b  21153  lssvs0or  21212  lvecinv  21215  ellspsn4  21226  lspdisjb  21228  islbs2  21256  islbs3  21257  dflidl2rng  21321  rngringbd  21419  isprmidlc  21443  prmidl0  21447  qsidom  21451  prmirredlem  21591  islindf3  21945  lindsmm  21947  lsslindf  21949  lsslinds  21950  issubassa  21986  sraassab  21987  issubassa2  22011  gsumbagdiag  22051  subrgasclcl  22187  ply1scleq  22434  matunit  22804  slesolinvbi  22807  en2top  23111  elcls  23199  neindisj2  23249  neiptopnei  23258  neiptopreu  23259  maxlp  23273  neitr  23306  iscncl  23395  cncnp  23406  isreg2  23503  dis2ndc  23586  1stccnp  23588  islly2  23610  dislly  23623  dissnlocfin  23655  kgencmp2  23672  pt1hmeo  23932  xkocnv  23940  t0kq  23944  uffixfr  24049  flimcf  24108  cnpflf2  24126  fclscf  24151  cnextf  24192  utopsnneiplem  24373  isucn2  24404  cfilucfil  24685  psmetutop  24693  restmetu  24696  tngngp2  24778  tngngp  24780  nmoleub  24857  metdseq0  24981  cnheibor  25083  pcophtb  25157  nmoleub2lem  25242  lmmbr  25386  iscfil3  25401  cmetss  25444  cldcss  25569  mbfeqalem2  25770  mbfposb  25781  itg2const2  25869  itgss3  25943  plyco0  26318  dgrlt  26392  ulm2  26514  coseq00topi  26633  coseq0negpitopi  26634  sineq0  26655  relogbcxpb  26918  atans2  27062  xrlimcnp  27099  dchrelbas2  27367  dchrn0  27380  2sqb  27562  nosupbnd2  27846  noinfbnd2  27861  lesrec  27958  ltmuls2  28330  elreno2  28654  istrkg2ld  28695  tgcgreqb  28716  tgbtwncomb  28724  trgcgrg  28750  legov  28820  legov2  28821  legov3  28833  hlbtwn  28846  tglineelsb2  28867  tglinecom  28870  colline  28885  mirinv  28905  mirbtwnb  28911  mirbtwnhl  28919  perpcom  28952  isperp2  28954  oppcom  28984  opphllem3  28989  lnopp2hpgb  29004  colopp  29010  colhp  29011  plngcplem  29025  plngrotlem2  29028  lmieu  29051  iscgra1  29078  dfcgra2  29098  edgnbusgreu  29658  nb3grprlem1  29671  lfgriswlk  29977  eleclclwwlknlem2  30353  clwwlknscsh  30354  clwwlknon1  30389  numclwwlk2lem1  30668  grpoinvid1  30821  grpoinvid2  30822  leopmul  32427  hst1h  32520  eqelbid  32762  diffib  32808  ifnebib  32836  iinabrex  32855  disjabrex  32868  disjabrexf  32869  erbr3b  32903  f1o3d  32912  funimass4f  32923  2ndimaxp  32932  fgreu  32957  fcnvgreu  32958  1stpreimas  32992  fcobij  33006  cocnvf1o  33015  resf1o  33016  nn0xmulclb  33057  fzsplit3  33079  fzo0opth  33089  sgnmulsgp  33117  eliccioo  33191  mgcmntco  33255  dfmgc2lem  33256  dfmgc2  33257  pwrssmgc  33261  mgcf1o  33264  mndlrinvb  33286  mndlactfo  33288  mndractfo  33290  mndlactf1o  33291  mndractf1o  33292  gsumhashmul  33328  gsumwrd2dccatlem  33338  cyc3genpm  33413  isarchi3  33448  prmsimpcyc  33489  elrgspnsubrunlem1  33508  elrgspnsubrun  33510  rlocisunit  33537  ricdomn  33551  isdrng4  33559  fracerl  33570  dvdsruasso  33642  dvdsruasso2  33643  dvdsrspss  33644  grplsmid  33657  quslsm  33658  nsgmgc  33665  nsgqusf1olem2  33667  nsgqusf1olem3  33668  pidlnzb  33674  unitpidl1  33676  elrspunidl  33680  elrspunsn  33681  drngidl  33685  drngidlhash  33686  mxidlirred  33700  mxidlnzrb  33707  qsdrng  33724  dflring3  33732  dflring4  33733  rsprprmprmidlb  33758  rprmirredb  33767  deg1le0eq0  33808  ply1unit  33810  0mplrim  33849  selvply1rhmlem2  33856  evlextv  33877  mplvrpmrhm  33882  esplyfv1  33904  esplyfval1  33908  esplyfvaln  33909  esplyind  33910  lvecdim0  33942  extdg1b  34002  fldextrspunlsp  34009  irngnzply1  34026  1smat1  34139  ist0cld  34168  qtophaus  34171  reff  34174  locfinreflem  34175  cmpcref  34185  zarcls1  34204  zarclsun  34205  zarclsiin  34206  zarclssn  34208  metider  34229  pstmfval  34231  qqhval2  34317  aean  34579  imambfm  34597  eulerpartlemgvv  34711  orvcgteel  34803  orvclteel  34808  ballotlemsf1o  34849  actfunsnf1o  34936  reprsuc  34947  reprpmtf1o  34958  sconnpi1  35630  brofs2  36468  brifs2  36469  broutsideof2  36513  ttc0elw  36927  bj-abv  37430  irrdiff  37858  ltflcei  38147  poimirlem25  38184  ismblfin  38200  cnambfre  38207  ftc1anclem6  38237  ismndo1  38412  isdrngo2  38497  eqvrelsymb  39229  eqvrelth  39234  lshpnelb  39648  lshpnel2N  39649  lsatspn0  39664  lsatelbN  39670  lsat0cv  39697  lcvexch  39703  lcv1  39705  lkrshp3  39770  lkrpssN  39827  lkrss2N  39833  cvlsupr2  40007  atcvrlln  40184  llncvrlpln  40222  2llnmj  40224  lplncvrlvol  40280  2lplnmj  40286  polcon2bN  40584  pcl0bN  40587  lhpmcvr3  40689  lhpmatb  40695  ltrncoidN  40792  ltrneq3  40872  ltrniotavalbN  41248  cdlemg1cN  41251  diclspsn  41858  dihopelvalcpre  41912  dihord4  41922  dihord  41928  dihmeetlem4preN  41970  dih1dimatlem0  41992  dochsscl  42032  dochoccl  42033  dochord  42034  dochsat  42047  dochshpncl  42048  dochsatshpb  42116  dochshpsat  42118  mapdval4N  42296  mapdsn  42305  hdmap14lem12  42543  hdmapip0  42579  hlhillcs  42622  resuppsinopn  43014  mulgt0b2d  43142  mullt0b1d  43147  mullt0b2d  43148  riccrng  43182  ricdrng  43189  prjspner1  43250  mrefg2  43330  mzpmfp  43370  lzenom  43393  elpell14qr2  43481  elpell1qr2  43491  pellfund14b  43518  congabseq  43593  acongeq  43602  jm2.23  43615  jm2.20nn  43616  jm2.25lem1  43617  wepwsolem  43661  islssfg2  43690  lnmlmic  43707  dfacbasgrp  43727  unielss  43837  rfovcnvf1od  44622  dssmapnvod  44638  ntrclscls00  44684  rfcnpre3  45645  rfcnpre4  45646  ssmapsn  45824  rnmptssbi  45867  infxrgelbrnmpt  46060  xnegre  46072  xrpnf  46091  rexanuz2nf  46098  ioossioobi  46125  iccshift  46126  iocopn  46128  eliccelioc  46129  iooshift  46130  icoopn  46133  qinioo  46143  limcdm0  46226  islptre  46227  islpcn  46245  limcresioolb  46249  climuzlem  46349  climlimsup  46366  liminfgelimsup  46388  liminfgelimsupuz  46394  climliminf  46412  climliminflimsup  46414  climliminflimsup2  46415  xlimpnfxnegmnf  46420  xlimbr  46433  xlimmnfv  46440  xlimpnfv  46444  xlimclim2  46446  dfxlim2v  46453  climresdm  46456  xlimresdm  46465  xlimliminflimsup  46468  fperdvper  46525  itgperiod  46587  fourierdlem32  46745  fourierdlem33  46746  fourierdlem48  46760  fourierdlem49  46761  fourierdlem71  46783  fourierdlem81  46793  preimagelt  47305  preimalegt  47306  smfliminflem  47436  smfliminfmpt  47438  chnsubseqwl  47487  fcoresfob  47698  m1mod0mod1  47986  uhgrimedg  48545  isubgr3stgrlem8  48627  rngcinvALTV  48930  ringcinvALTV  48964  xpco2  49520  fvconstr  49525  fvconstrn0  49526  lubeldm2  49619  glbeldm2  49620  upeu2lem  49691  sectpropd  49700  invpropd  49702  isopropd  49704  cicerALT  49709  cicpropd  49713  up1st2ndb  49850  uobffth  49881  uobeqw  49882  natoppfb  49894  oppc1stflem  49950  fucofulem1  49973  functhinclem1  50107  fullthinc  50113  thincciso4  50120  thinciso  50133  functermclem  50170  termcterm3  50178  termcciso  50179  termcarweu  50191  termfucterm  50207  prstchom2ALT  50227  lanval2  50290  ranval2  50293