Theorem impbida 801

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  823  bibiad  840  eqrdav  2736  eqsndOLD  4789  frsn  5720  funfvbrb  7005  iinpreima  7023  fcdmssb  7076  fnprb  7164  fntpb  7165  fpr2g  7167  nvocnv  7237  fsnex  7239  f1ocnv2d  7621  resf1extb  7886  el2xptp0  7990  1stconst  8052  2ndconst  8053  cnvf1o  8063  fimaproj  8087  tfrlem15  8333  oeeui  8540  ersymb  8660  swoer  8677  erth  8700  boxriin  8890  boxcutc  8891  domunsncan  9017  pw2f1olem  9021  enen1  9057  enen2  9058  domen1  9059  domen2  9060  sdomen1  9061  sdomen2  9062  xpmapenlem  9084  ensymfib  9120  ordiso2  9432  wdomen1  9493  wdomen2  9494  fin23lem26  10247  fpwwe2lem7  10560  r1wunlim  10660  mul2lt0bi  13025  ixxun  13289  xov1plusxeqvd  13426  fzsplit2  13477  fseq1p1m1  13526  elfz2nn0  13546  flflp1  13739  modaddb  13841  modsubdir  13875  zesq  14161  expnngt1b  14177  hashprg  14330  hashgt0elexb  14337  hashbclem  14387  hashge2el2difb  14417  rereb  15055  rlimclim  15481  iserex  15592  caucvgb  15615  mptfzshft  15713  fsumrev  15714  climcnds  15786  fprodrev  15912  dvdsadd2b  16245  nn0ob  16323  bitsfzo  16374  dfgcd2  16485  dvdsmulgcd  16495  lcmgcdeq  16551  qden1elz  16696  mrcidb  17550  mrieqvlemd  17564  isacs2  17588  cicer  17742  ssclem  17755  issubc3  17785  ffthiso  17867  fuciso  17914  setcmon  18023  setcepi  18024  setcinv  18026  catciso  18047  acsfiindd  18488  issstrmgm  18590  mgmhmf1o  18637  issubmgm2  18640  subsubmgm  18647  resmgmhm2b  18650  issubmnd  18698  mhmf1o  18733  subsubm  18753  resmhm2b  18759  grpinvid1  18933  grpinvid2  18934  subsubg  19091  ssnmz  19107  ghmf1  19187  kerf1ghm  19188  ghmf1o  19189  conjnmzb  19194  subggim  19207  gicsubgen  19220  ghmqusnsglem1  19221  ghmquskerlem1  19224  ghmqusker  19228  gass  19242  odf1  19503  gex1  19532  fislw  19566  sylow3lem2  19569  sylow3lem6  19573  lsmdisj2a  19628  lsmdisj2b  19629  efgred2  19694  dmdprdsplit  19990  2nsgsimpgd  20045  simpgnsgbid  20046  ablsimpgd  20059  ogrpinv0le  20077  ogrpaddltbi  20080  ogrpaddltrbid  20082  ogrpinv0lt  20084  0unit  20344  irrednegb  20379  rnghmf1o  20400  rhmf1o  20438  subsubrng  20508  subrgunit  20535  subsubrg  20543  rngcinv  20582  ringcinv  20616  isdrng2  20688  issubdrg  20725  islss3  20922  islss4  20925  ellspsn6  20957  lspsneq0b  20976  islmhm2  21002  lmhmf1o  21010  reslmhm2b  21018  lssvs0or  21077  lvecinv  21080  ellspsn4  21091  lspdisjb  21093  islbs2  21121  islbs3  21122  dflidl2rng  21185  rngringbd  21275  prmirredlem  21439  islindf3  21793  lindsmm  21795  lsslindf  21797  lsslinds  21798  issubassa  21834  sraassab  21835  issubassa2  21860  gsumbagdiag  21899  subrgasclcl  22034  ply1scleq  22261  matunit  22634  slesolinvbi  22637  en2top  22941  elcls  23029  neindisj2  23079  neiptopnei  23088  neiptopreu  23089  maxlp  23103  neitr  23136  iscncl  23225  cncnp  23236  isreg2  23333  dis2ndc  23416  1stccnp  23418  islly2  23440  dislly  23453  dissnlocfin  23485  kgencmp2  23502  pt1hmeo  23762  xkocnv  23770  t0kq  23774  uffixfr  23879  flimcf  23938  cnpflf2  23956  fclscf  23981  cnextf  24022  utopsnneiplem  24203  isucn2  24234  cfilucfil  24515  psmetutop  24523  restmetu  24526  tngngp2  24608  tngngp  24610  nmoleub  24687  metdseq0  24811  cnheibor  24922  pcophtb  24997  nmoleub2lem  25082  lmmbr  25226  iscfil3  25241  cmetss  25284  cldcss  25409  mbfeqalem2  25611  mbfposb  25622  itg2const2  25710  itgss3  25784  plyco0  26165  dgrlt  26240  ulm2  26362  coseq00topi  26479  coseq0negpitopi  26480  sineq0  26501  relogbcxpb  26765  atans2  26909  xrlimcnp  26946  dchrelbas2  27216  dchrn0  27229  2sqb  27411  nosupbnd2  27696  noinfbnd2  27711  lesrec  27807  ltmuls2  28179  elreno2  28503  istrkg2ld  28544  tgcgreqb  28565  tgbtwncomb  28573  trgcgrg  28599  legov  28669  legov2  28670  legov3  28682  hlbtwn  28695  tglineelsb2  28716  tglinecom  28719  colline  28733  mirinv  28750  mirbtwnb  28756  mirbtwnhl  28764  perpcom  28797  isperp2  28799  oppcom  28828  opphllem3  28833  lnopp2hpgb  28847  colopp  28853  colhp  28854  lmieu  28868  iscgra1  28894  dfcgra2  28914  edgnbusgreu  29452  nb3grprlem1  29465  lfgriswlk  29772  eleclclwwlknlem2  30148  clwwlknscsh  30149  clwwlknon1  30184  numclwwlk2lem1  30463  grpoinvid1  30616  grpoinvid2  30617  leopmul  32222  hst1h  32315  eqelbid  32561  diffib  32608  ifnebib  32636  iinabrex  32656  disjabrex  32669  disjabrexf  32670  erbr3b  32707  f1o3d  32716  funimass4f  32727  2ndimaxp  32736  fgreu  32761  fcnvgreu  32762  1stpreimas  32796  fcobij  32810  cocnvf1o  32819  resf1o  32820  nn0xmulclb  32862  fzsplit3  32884  fzo0opth  32894  sgn3da  32926  sgnnbi  32930  sgnpbi  32931  sgnmulsgn  32934  sgnmulsgp  32935  eliccioo  33023  mgcmntco  33087  dfmgc2lem  33088  dfmgc2  33089  pwrssmgc  33093  mgcf1o  33096  mndlrinvb  33118  mndlactfo  33120  mndractfo  33122  mndlactf1o  33123  mndractf1o  33124  gsumhashmul  33161  gsumwrd2dccatlem  33171  cyc3genpm  33246  isarchi3  33281  prmsimpcyc  33322  elrgspnsubrunlem1  33341  elrgspnsubrun  33343  domnlcanbOLD  33375  isdrng4  33389  fracerl  33400  qsxpid  33455  dvdsruasso  33478  dvdsruasso2  33479  dvdsrspss  33480  grplsmid  33497  quslsm  33498  nsgmgc  33505  nsgqusf1olem2  33507  nsgqusf1olem3  33508  pidlnzb  33515  unitpidl1  33517  elrspunidl  33521  elrspunsn  33522  drngidl  33526  drngidlhash  33527  isprmidlc  33540  prmidl0  33543  qsidom  33547  mxidlirred  33565  mxidlnzrb  33573  qsdrng  33590  rsprprmprmidlb  33616  rprmirredb  33625  deg1le0eq0  33666  ply1unit  33668  evlextv  33719  mplvrpmrhm  33724  esplyfv1  33746  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  lvecdim0  33784  extdg1b  33845  fldextrspunlsp  33852  irngnzply1  33869  1smat1  33982  ist0cld  34011  qtophaus  34014  reff  34017  locfinreflem  34018  cmpcref  34028  zarcls1  34047  zarclsun  34048  zarclsiin  34049  zarclssn  34051  metider  34072  pstmfval  34074  qqhval2  34160  aean  34422  imambfm  34440  eulerpartlemgvv  34554  orvcgteel  34646  orvclteel  34651  ballotlemsf1o  34692  actfunsnf1o  34782  reprsuc  34793  reprpmtf1o  34804  sconnpi1  35455  brofs2  36293  brifs2  36294  broutsideof2  36338  bj-abv  37154  irrdiff  37581  ltflcei  37859  poimirlem25  37896  ismblfin  37912  cnambfre  37919  ftc1anclem6  37949  ismndo1  38124  isdrngo2  38209  eqvrelsymb  38941  eqvrelth  38946  lshpnelb  39360  lshpnel2N  39361  lsatspn0  39376  lsatelbN  39382  lsat0cv  39409  lcvexch  39415  lcv1  39417  lkrshp3  39482  lkrpssN  39539  lkrss2N  39545  cvlsupr2  39719  atcvrlln  39896  llncvrlpln  39934  2llnmj  39936  lplncvrlvol  39992  2lplnmj  39998  polcon2bN  40296  pcl0bN  40299  lhpmcvr3  40401  lhpmatb  40407  ltrncoidN  40504  ltrneq3  40584  ltrniotavalbN  40960  cdlemg1cN  40963  diclspsn  41570  dihopelvalcpre  41624  dihord4  41634  dihord  41640  dihmeetlem4preN  41682  dih1dimatlem0  41704  dochsscl  41744  dochoccl  41745  dochord  41746  dochsat  41759  dochshpncl  41760  dochsatshpb  41828  dochshpsat  41830  mapdval4N  42008  mapdsn  42017  hdmap14lem12  42255  hdmapip0  42291  hlhillcs  42334  resuppsinopn  42733  mulgt0b2d  42848  mullt0b1d  42853  mullt0b2d  42854  riccrng  42892  ricdrng  42899  prjspner1  42984  mrefg2  43064  mzpmfp  43104  lzenom  43127  elpell14qr2  43219  elpell1qr2  43229  pellfund14b  43256  congabseq  43331  acongeq  43340  jm2.23  43353  jm2.20nn  43354  jm2.25lem1  43355  wepwsolem  43399  islssfg2  43428  lnmlmic  43445  dfacbasgrp  43465  unielss  43575  rfovcnvf1od  44360  dssmapnvod  44376  ntrclscls00  44422  rfcnpre3  45393  rfcnpre4  45394  ssmapsn  45574  rnmptssbi  45618  infxrgelbrnmpt  45812  xnegre  45824  xrpnf  45843  rexanuz2nf  45850  ioossioobi  45877  iccshift  45878  iocopn  45880  eliccelioc  45881  iooshift  45882  icoopn  45885  qinioo  45895  limcdm0  45978  islptre  45979  islpcn  45997  limcresioolb  46001  climuzlem  46101  climlimsup  46118  liminfgelimsup  46140  liminfgelimsupuz  46146  climliminf  46164  climliminflimsup  46166  climliminflimsup2  46167  xlimpnfxnegmnf  46172  xlimbr  46185  xlimmnfv  46192  xlimpnfv  46196  xlimclim2  46198  dfxlim2v  46205  climresdm  46208  xlimresdm  46217  xlimliminflimsup  46220  fperdvper  46277  itgperiod  46339  fourierdlem32  46497  fourierdlem33  46498  fourierdlem48  46512  fourierdlem49  46513  fourierdlem71  46535  fourierdlem81  46545  preimagelt  47057  preimalegt  47058  smfliminflem  47188  smfliminfmpt  47190  chnsubseqwl  47237  fcoresfob  47432  m1mod0mod1  47714  uhgrimedg  48251  isubgr3stgrlem8  48333  rngcinvALTV  48636  ringcinvALTV  48670  xpco2  49216  fvconstr  49221  fvconstrn0  49222  lubeldm2  49315  glbeldm2  49316  upeu2lem  49387  sectpropd  49396  invpropd  49398  isopropd  49400  cicerALT  49405  cicpropd  49409  up1st2ndb  49546  uobffth  49577  uobeqw  49578  natoppfb  49590  oppc1stflem  49646  fucofulem1  49669  functhinclem1  49803  fullthinc  49809  thincciso4  49816  thinciso  49829  functermclem  49866  termcterm3  49874  termcciso  49875  termcarweu  49887  termfucterm  49903  prstchom2ALT  49923  lanval2  49986  ranval2  49989