Theorem impbida 810

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  biadanid  832  bibiad  850  eqsndOLD  4789  frsn  5735  funfvbrb  7032  iinpreima  7050  fcdmssb  7103  fnprb  7192  fntpb  7193  fpr2g  7195  nvocnv  7265  fsnex  7267  f1ocnv2d  7649  resf1extb  7915  el2xptp0  8017  1stconst  8079  2ndconst  8080  cnvf1o  8090  fimaproj  8115  tfrlem15  8363  oeeui  8572  ersymb  8693  swoer  8710  erth  8733  boxriin  8922  boxcutc  8923  domunsncan  9049  pw2f1olem  9053  enen1  9089  enen2  9090  domen1  9091  domen2  9092  sdomen1  9093  sdomen2  9094  xpmapenlem  9116  ensymfib  9152  ordiso2  9463  wdomen1  9524  wdomen2  9525  fin23lem26  10282  fpwwe2lem7  10595  r1wunlim  10695  mul2lt0bi  13101  ixxun  13365  xov1plusxeqvd  13502  fzsplit2  13554  fseq1p1m1  13603  elfz2nn0  13623  flflp1  13817  modaddb  13919  modsubdir  13953  zesq  14239  expnngt1b  14255  hashprg  14408  hashgt0elexb  14415  hashbclem  14465  hashge2el2difb  14495  sgn3da  15114  sgnnbi  15117  sgnpbi  15118  sgnmulsgn  15122  rereb  15147  rlimclim  15573  iserex  15684  caucvgb  15707  mptfzshft  15805  fsumrev  15806  climcnds  15881  fprodrev  16007  dvdsadd2b  16340  nn0ob  16418  bitsfzo  16469  dfgcd2  16580  dvdsmulgcd  16590  lcmgcdeq  16646  qden1elz  16792  mrcidb  17647  mrieqvlemd  17661  isacs2  17685  cicer  17839  ssclem  17852  issubc3  17882  ffthiso  17964  fuciso  18011  setcmon  18120  setcepi  18121  setcinv  18123  catciso  18144  acsfiindd  18585  issstrmgm  18687  mgmhmf1o  18734  issubmgm2  18737  subsubmgm  18744  resmgmhm2b  18747  issubmnd  18795  mhmf1o  18830  subsubm  18850  resmhm2b  18856  grpinvid1  19033  grpinvid2  19034  subsubg  19191  ssnmz  19207  ghmf1  19286  kerf1ghm  19287  ghmf1o  19288  conjnmzb  19293  subggim  19306  gicsubgen  19319  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmqusker  19327  gass  19341  odf1  19602  gex1  19631  fislw  19665  sylow3lem2  19668  sylow3lem6  19672  lsmdisj2a  19727  lsmdisj2b  19728  efgred2  19793  dmdprdsplit  20089  2nsgsimpgd  20144  simpgnsgbid  20145  ablsimpgd  20158  ogrpinv0le  20176  ogrpaddltbi  20179  ogrpaddltrbid  20181  ogrpinv0lt  20183  0unit  20445  irrednegb  20480  rnghmf1o  20501  rhmf1o  20540  subsubrng  20613  subrgunit  20640  subsubrg  20648  rngcinv  20687  ringcinv  20721  isdrng2  20793  issubdrg  20829  islss3  21026  islss4  21029  ellspsn6  21061  lspsneq0b  21080  islmhm2  21105  lmhmf1o  21113  reslmhm2b  21121  lssvs0or  21180  lvecinv  21183  ellspsn4  21194  lspdisjb  21196  islbs2  21224  islbs3  21225  dflidl2rng  21288  rngringbd  21378  prmirredlem  21524  islindf3  21878  lindsmm  21880  lsslindf  21882  lsslinds  21883  issubassa  21919  sraassab  21920  issubassa2  21944  gsumbagdiag  21984  subrgasclcl  22120  ply1scleq  22368  matunit  22738  slesolinvbi  22741  en2top  23045  elcls  23133  neindisj2  23183  neiptopnei  23192  neiptopreu  23193  maxlp  23207  neitr  23240  iscncl  23329  cncnp  23340  isreg2  23437  dis2ndc  23520  1stccnp  23522  islly2  23544  dislly  23557  dissnlocfin  23589  kgencmp2  23606  pt1hmeo  23866  xkocnv  23874  t0kq  23878  uffixfr  23983  flimcf  24042  cnpflf2  24060  fclscf  24085  cnextf  24126  utopsnneiplem  24307  isucn2  24338  cfilucfil  24619  psmetutop  24627  restmetu  24630  tngngp2  24712  tngngp  24714  nmoleub  24791  metdseq0  24915  cnheibor  25017  pcophtb  25091  nmoleub2lem  25176  lmmbr  25320  iscfil3  25335  cmetss  25378  cldcss  25503  mbfeqalem2  25704  mbfposb  25715  itg2const2  25803  itgss3  25877  plyco0  26252  dgrlt  26326  ulm2  26448  coseq00topi  26567  coseq0negpitopi  26568  sineq0  26589  relogbcxpb  26852  atans2  26996  xrlimcnp  27033  dchrelbas2  27301  dchrn0  27314  2sqb  27496  nosupbnd2  27780  noinfbnd2  27795  lesrec  27892  ltmuls2  28264  elreno2  28588  istrkg2ld  28629  tgcgreqb  28650  tgbtwncomb  28658  trgcgrg  28684  legov  28754  legov2  28755  legov3  28767  hlbtwn  28780  tglineelsb2  28801  tglinecom  28804  colline  28819  mirinv  28839  mirbtwnb  28845  mirbtwnhl  28853  perpcom  28886  isperp2  28888  oppcom  28917  opphllem3  28922  lnopp2hpgb  28936  colopp  28942  colhp  28943  lmieu  28957  plngcplem  28992  plngrotlem2  28995  iscgra1  29004  dfcgra2  29024  edgnbusgreu  29568  nb3grprlem1  29581  lfgriswlk  29887  eleclclwwlknlem2  30263  clwwlknscsh  30264  clwwlknon1  30299  numclwwlk2lem1  30578  grpoinvid1  30731  grpoinvid2  30732  leopmul  32337  hst1h  32430  eqelbid  32674  diffib  32720  ifnebib  32748  iinabrex  32769  disjabrex  32782  disjabrexf  32783  erbr3b  32819  f1o3d  32828  funimass4f  32839  2ndimaxp  32848  fgreu  32873  fcnvgreu  32874  1stpreimas  32908  fcobij  32922  cocnvf1o  32931  resf1o  32932  nn0xmulclb  32973  fzsplit3  32995  fzo0opth  33005  sgnmulsgp  33034  eliccioo  33108  mgcmntco  33172  dfmgc2lem  33173  dfmgc2  33174  pwrssmgc  33178  mgcf1o  33181  mndlrinvb  33203  mndlactfo  33205  mndractfo  33207  mndlactf1o  33208  mndractf1o  33209  gsumhashmul  33247  gsumwrd2dccatlem  33257  cyc3genpm  33332  isarchi3  33367  prmsimpcyc  33408  elrgspnsubrunlem1  33428  elrgspnsubrun  33430  rlocisunit  33457  domnlcanbOLD  33465  ricdomn  33474  isdrng4  33482  fracerl  33493  qsxpid  33548  dvdsruasso  33571  dvdsruasso2  33572  dvdsrspss  33573  grplsmid  33590  quslsm  33591  nsgmgc  33598  nsgqusf1olem2  33600  nsgqusf1olem3  33601  pidlnzb  33608  unitpidl1  33610  elrspunidl  33614  elrspunsn  33615  drngidl  33619  drngidlhash  33620  isprmidlc  33633  prmidl0  33637  qsidom  33641  mxidlirred  33660  mxidlnzrb  33668  qsdrng  33685  dflring3  33693  dflring4  33694  rsprprmprmidlb  33719  rprmirredb  33728  deg1le0eq0  33769  ply1unit  33771  0mplrim  33811  selvply1rhmlem2  33818  evlextv  33839  mplvrpmrhm  33844  esplyfv1  33866  esplyfval1  33870  esplyfvaln  33871  esplyind  33872  lvecdim0  33904  extdg1b  33964  fldextrspunlsp  33971  irngnzply1  33988  1smat1  34101  ist0cld  34130  qtophaus  34133  reff  34136  locfinreflem  34137  cmpcref  34147  zarcls1  34166  zarclsun  34167  zarclsiin  34168  zarclssn  34170  metider  34191  pstmfval  34193  qqhval2  34279  aean  34541  imambfm  34559  eulerpartlemgvv  34673  orvcgteel  34765  orvclteel  34770  ballotlemsf1o  34811  actfunsnf1o  34898  reprsuc  34909  reprpmtf1o  34920  sconnpi1  35589  brofs2  36427  brifs2  36428  broutsideof2  36472  ttc0elw  36887  bj-abv  37391  irrdiff  37818  ltflcei  38107  poimirlem25  38144  ismblfin  38160  cnambfre  38167  ftc1anclem6  38197  ismndo1  38372  isdrngo2  38457  eqvrelsymb  39189  eqvrelth  39194  lshpnelb  39608  lshpnel2N  39609  lsatspn0  39624  lsatelbN  39630  lsat0cv  39657  lcvexch  39663  lcv1  39665  lkrshp3  39730  lkrpssN  39787  lkrss2N  39793  cvlsupr2  39967  atcvrlln  40144  llncvrlpln  40182  2llnmj  40184  lplncvrlvol  40240  2lplnmj  40246  polcon2bN  40544  pcl0bN  40547  lhpmcvr3  40649  lhpmatb  40655  ltrncoidN  40752  ltrneq3  40832  ltrniotavalbN  41208  cdlemg1cN  41211  diclspsn  41818  dihopelvalcpre  41872  dihord4  41882  dihord  41888  dihmeetlem4preN  41930  dih1dimatlem0  41952  dochsscl  41992  dochoccl  41993  dochord  41994  dochsat  42007  dochshpncl  42008  dochsatshpb  42076  dochshpsat  42078  mapdval4N  42256  mapdsn  42265  hdmap14lem12  42503  hdmapip0  42539  hlhillcs  42582  resuppsinopn  42972  mulgt0b2d  43100  mullt0b1d  43105  mullt0b2d  43106  riccrng  43140  ricdrng  43147  prjspner1  43208  mrefg2  43288  mzpmfp  43328  lzenom  43351  elpell14qr2  43439  elpell1qr2  43449  pellfund14b  43476  congabseq  43551  acongeq  43560  jm2.23  43573  jm2.20nn  43574  jm2.25lem1  43575  wepwsolem  43619  islssfg2  43648  lnmlmic  43665  dfacbasgrp  43685  unielss  43795  rfovcnvf1od  44580  dssmapnvod  44596  ntrclscls00  44642  rfcnpre3  45613  rfcnpre4  45614  ssmapsn  45792  rnmptssbi  45835  infxrgelbrnmpt  46028  xnegre  46040  xrpnf  46059  rexanuz2nf  46066  ioossioobi  46093  iccshift  46094  iocopn  46096  eliccelioc  46097  iooshift  46098  icoopn  46101  qinioo  46111  limcdm0  46194  islptre  46195  islpcn  46213  limcresioolb  46217  climuzlem  46317  climlimsup  46334  liminfgelimsup  46356  liminfgelimsupuz  46362  climliminf  46380  climliminflimsup  46382  climliminflimsup2  46383  xlimpnfxnegmnf  46388  xlimbr  46401  xlimmnfv  46408  xlimpnfv  46412  xlimclim2  46414  dfxlim2v  46421  climresdm  46424  xlimresdm  46433  xlimliminflimsup  46436  fperdvper  46493  itgperiod  46555  fourierdlem32  46713  fourierdlem33  46714  fourierdlem48  46728  fourierdlem49  46729  fourierdlem71  46751  fourierdlem81  46761  preimagelt  47273  preimalegt  47274  smfliminflem  47404  smfliminfmpt  47406  chnsubseqwl  47455  fcoresfob  47666  m1mod0mod1  47954  uhgrimedg  48513  isubgr3stgrlem8  48595  rngcinvALTV  48898  ringcinvALTV  48932  xpco2  49478  fvconstr  49483  fvconstrn0  49484  lubeldm2  49577  glbeldm2  49578  upeu2lem  49649  sectpropd  49658  invpropd  49660  isopropd  49662  cicerALT  49667  cicpropd  49671  up1st2ndb  49808  uobffth  49839  uobeqw  49840  natoppfb  49852  oppc1stflem  49908  fucofulem1  49931  functhinclem1  50065  fullthinc  50071  thincciso4  50078  thinciso  50091  functermclem  50128  termcterm3  50136  termcciso  50137  termcarweu  50149  termfucterm  50165  prstchom2ALT  50185  lanval2  50248  ranval2  50251