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  5743  funfvbrb  7058  iinpreima  7077  fcdmssb  7130  fnprb  7221  fntpb  7222  fpr2g  7224  nvocnv  7296  fsnex  7298  f1ocnv2d  7681  resf1extb  7953  el2xptp0  8054  1stconst  8121  2ndconst  8122  cnvf1o  8132  fimaproj  8162  tfrlem15  8411  oeeui  8622  ersymb  8743  swoer  8760  erth  8783  boxriin  8979  boxcutc  8980  domunsncan  9107  pw2f1olem  9111  enen1  9147  enen2  9148  domen1  9149  domen2  9150  sdomen1  9151  sdomen2  9152  xpmapenlem  9174  ensymfib  9210  ordiso2  9519  wdomen1  9580  wdomen2  9581  fin23lem26  10413  fpwwe2lem7  10732  r1wunlim  10832  mul2lt0bi  13238  ixxun  13502  xov1plusxeqvd  13639  fzsplit2  13693  fseq1p1m1  13742  elfz2nn0  13762  flflp1  13957  modaddb  14059  modsubdir  14093  zesq  14380  expnngt1b  14396  hashprg  14549  hashgt0elexb  14556  hashbclem  14607  hashge2el2difb  14637  sgn3da  15266  sgnnbi  15269  sgnpbi  15270  sgnmulsgn  15274  rereb  15299  rlimclim  15725  iserex  15836  caucvgb  15859  mptfzshft  15956  fsumrev  15957  climcnds  16032  fprodrev  16156  dvdsadd2b  16488  nn0ob  16566  bitsfzo  16617  dfgcd2  16731  dvdsmulgcd  16742  lcmgcdeq  16799  qden1elz  16945  mrcidb  17801  mrieqvlemd  17815  isacs2  17839  cicer  17993  ssclem  18006  issubc3  18036  ffthiso  18118  fuciso  18165  setcmon  18274  setcepi  18275  setcinv  18277  catciso  18298  acsfiindd  18739  issstrmgm  18843  mgmhmf1o  18901  issubmgm2  18904  subsubmgm  18911  resmgmhm2b  18914  issubmnd  18965  mhmf1o  19003  subsubm  19024  resmhm2b  19030  grpinvid1  19214  grpinvid2  19215  subsubg  19372  ssnmz  19388  qsxpid  19399  ghmf1  19472  kerf1ghm  19473  ghmf1o  19474  conjnmzb  19479  subggim  19492  gicsubgen  19505  ghmqusnsglem1  19506  ghmquskerlem1  19509  ghmqusker  19513  gass  19527  odf1  19788  gex1  19817  fislw  19851  sylow3lem2  19854  sylow3lem6  19858  lsmdisj2a  19913  lsmdisj2b  19914  efgred2  19979  dmdprdsplit  20275  2nsgsimpgd  20330  simpgnsgbid  20331  ablsimpgd  20344  ogrpinv0le  20362  ogrpaddltbi  20365  ogrpaddltrbid  20367  ogrpinv0lt  20369  0unit  20638  irrednegb  20673  rnghmf1o  20694  rhmf1o  20739  subsubrng  20827  subrgunit  20854  subsubrg  20862  rngcinv  20901  ringcinv  20935  isdrng4  21004  isdrng3  21019  issubdrg  21049  islss3  21246  islss4  21249  ellspsn6  21281  lspsneq0b  21300  islmhm2  21325  lmhmf1o  21333  reslmhm2b  21341  lssvs0or  21400  lvecinv  21403  ellspsn4  21414  lspdisjb  21416  islbs2  21444  islbs3  21445  dflidl2rng  21509  drngidl  21551  rngringbd  21616  isprmidlc  21640  prmidl0  21646  qsidom  21650  prmirredlem  21790  islindf3  22144  lindsmm  22146  lsslindf  22148  lsslinds  22149  issubassa  22187  sraassab  22188  issubassa2  22212  gsumbagdiag  22252  subrgasclcl  22388  ply1scleq  22635  matunit  23005  slesolinvbi  23011  en2top  23315  elcls  23403  neindisj2  23453  neiptopnei  23462  neiptopreu  23463  maxlp  23477  neitr  23510  iscncl  23599  cncnp  23610  isreg2  23707  dis2ndc  23791  1stccnp  23793  islly2  23815  dislly  23828  dissnlocfin  23860  kgencmp2  23877  pt1hmeo  24137  xkocnv  24145  t0kq  24149  uffixfr  24254  flimcf  24313  cnpflf2  24331  fclscf  24356  cnextf  24397  utopsnneiplem  24578  isucn2  24609  cfilucfil  24890  psmetutop  24898  restmetu  24901  tngngp2  24983  tngngp  24985  nmoleub  25062  metdseq0  25186  cnheibor  25288  pcophtb  25362  nmoleub2lem  25447  lmmbr  25591  iscfil3  25606  cmetss  25649  cldcss  25774  mbfeqalem2  25975  mbfposb  25986  itg2const2  26074  itgss3  26147  plyco0  26522  dgrlt  26597  ulm2  26724  coseq00topi  26843  coseq0negpitopi  26844  sineq0  26864  relogbcxpb  27127  atans2  27271  xrlimcnp  27308  dchrelbas2  27576  dchrn0  27589  2sqb  27771  nosupbnd2  28085  noinfbnd2  28100  lesrec  28197  ltmuls2  28569  elreno2  28893  istrkg2ld  28934  tgcgreqb  28955  tgbtwncomb  28964  trgcgrg  28990  legov  29060  legov2  29061  legov3  29073  hlbtwn  29089  tglineelsb2  29112  tglinecom  29115  colline  29130  mirinv  29150  mirbtwnb  29156  mirbtwnhl  29164  mirleqb  29178  perpcom  29200  isperp2  29202  oppcom  29232  opphllem3  29237  lnopp2hpgb  29253  colopp  29259  colhp  29260  plngcplem  29275  plngrotlem2  29278  lmieu  29301  iscgra1  29329  dfcgra2  29350  ragsupplcgra  29357  cgraer  29389  angmgmaddeu1  29391  angmgmaddeu2  29392  angmgmaddeu3  29393  angmgmaddeu4  29394  angmgmaddeu5  29395  angmgmaddeu6  29396  angmgmaddeu7  29397  angmgmaddov2lem  29399  angmgmaddcpbl  29402  dfprlng2  29437  edgnbusgreu  29960  nb3grprlem1  29973  lfgriswlk  30283  eleclclwwlknlem2  30664  clwwlknscsh  30665  clwwlknon1  30700  numclwwlk2lem1  30989  grpoinvid1  31142  grpoinvid2  31143  leopmul  32748  hst1h  32841  eqelbid  33125  diffib  33171  ifnebib  33199  iinabrex  33217  disjabrex  33230  disjabrexf  33231  erbr3b  33265  f1o3d  33274  funimass4f  33285  2ndimaxp  33294  fgreu  33319  fcnvgreu  33320  1stpreimas  33353  fcobij  33365  cocnvf1o  33374  resf1o  33375  nn0xmulclb  33416  fzsplit3  33438  fzo0opth  33448  sgnmulsgp  33476  eliccioo  33550  mgcmntco  33608  dfmgc2lem  33609  dfmgc2  33610  pwrssmgc  33614  mgcf1o  33617  mndlrinvb  33639  mndlactfo  33641  mndractfo  33643  mndlactf1o  33644  mndractf1o  33645  gsumhashmul  33681  gsumwrd2dccatlem  33691  cyc3genpm  33766  isarchi3  33801  prmsimpcyc  33842  elrgspnsubrunlem1  33861  elrgspnsubrun  33863  rlocisunit  33890  ricdomn  33904  fracerl  33921  dvdsruasso  33993  dvdsruasso2  33994  dvdsrspss  33995  grplsmid  34008  quslsm  34009  nsgmgc  34016  nsgqusf1olem2  34018  nsgqusf1olem3  34019  pidlnzb  34025  unitpidl1  34027  elrspunidl  34031  elrspunsn  34032  drngidlhash  34036  mxidlirred  34050  mxidlnzrb  34057  qsdrng  34074  dflring3  34082  dflring4  34083  rsprprmprmidlb  34108  rprmirredb  34117  deg1le0eq0  34158  ply1unit  34160  0mplrim  34199  selvply1rhmlem2  34206  evlextv  34227  mplvrpmrhm  34232  esplyfv1  34254  esplyfval1  34258  esplyfvaln  34259  esplyind  34260  lvecdim0  34292  extdg1b  34352  fldextrspunlsp  34359  irngnzply1  34376  1smat1  34489  ist0cld  34518  qtophaus  34521  reff  34524  locfinreflem  34525  cmpcref  34535  zarcls1  34554  zarclsun  34555  zarclsiin  34556  zarclssn  34558  metider  34579  pstmfval  34581  qqhval2  34667  aean  34930  imambfm  34947  eulerpartlemgvv  35061  orvcgteel  35153  orvclteel  35158  ballotlemsf1o  35199  actfunsnf1o  35286  reprsuc  35297  reprpmtf1o  35308  erscottd  35822  sconnpi1  36125  brofs2  36969  brifs2  36970  broutsideof2  37014  ttc0elw  37442  bj-abv  37945  irrdiff  38387  ltflcei  38671  poimirlem25  38703  ismblfin  38719  cnambfre  38726  ftc1anclem6  38756  ismndo1  38947  isdrngo2  39032  eqvrelsymb  39762  eqvrelth  39767  lshpnelb  40181  lshpnel2N  40182  lsatspn0  40197  lsatelbN  40203  lsat0cv  40230  lcvexch  40236  lcv1  40238  lkrshp3  40303  lkrpssN  40360  lkrss2N  40366  cvlsupr2  40540  atcvrlln  40717  llncvrlpln  40755  2llnmj  40757  lplncvrlvol  40813  2lplnmj  40819  polcon2bN  41117  pcl0bN  41120  lhpmcvr3  41222  lhpmatb  41228  ltrncoidN  41325  ltrneq3  41405  ltrniotavalbN  41781  cdlemg1cN  41784  diclspsn  42391  dihopelvalcpre  42445  dihord4  42455  dihord  42461  dihmeetlem4preN  42503  dih1dimatlem0  42525  dochsscl  42565  dochoccl  42566  dochord  42567  dochsat  42580  dochshpncl  42581  dochsatshpb  42649  dochshpsat  42651  mapdval4N  42829  mapdsn  42838  hdmap14lem12  43076  hdmapip0  43112  hlhillcs  43155  resuppsinopn  43554  mulgt0b2d  43682  mullt0b1d  43687  mullt0b2d  43688  riccrng  43723  ricdrng  43733  prjspnnorm  43801  mrefg2  43858  mzpmfp  43898  lzenom  43921  elpell14qr2  44009  elpell1qr2  44019  pellfund14b  44046  congabseq  44121  acongeq  44130  jm2.23  44143  jm2.20nn  44144  jm2.25lem1  44145  wepwsolem  44189  islssfg2  44213  lnmlmic  44230  dfacbasgrp  44250  unielss  44360  rfovcnvf1od  45144  dssmapnvod  45160  ntrclscls00  45206  rfcnpre3  46189  rfcnpre4  46190  ssmapsn  46368  rnmptssbi  46411  infxrgelbrnmpt  46603  xnegre  46615  xrpnf  46634  rexanuz2nf  46641  ioossioobi  46668  iccshift  46669  iocopn  46671  eliccelioc  46672  iooshift  46673  icoopn  46676  qinioo  46686  limcdm0  46769  islptre  46770  islpcn  46788  limcresioolb  46792  climuzlem  46892  climlimsup  46909  liminfgelimsup  46931  liminfgelimsupuz  46937  climliminf  46955  climliminflimsup  46957  climliminflimsup2  46958  xlimpnfxnegmnf  46963  xlimbr  46976  xlimmnfv  46983  xlimpnfv  46987  xlimclim2  46989  dfxlim2v  46996  climresdm  46999  xlimresdm  47008  xlimliminflimsup  47011  fperdvper  47068  itgperiod  47130  fourierdlem32  47288  fourierdlem33  47289  fourierdlem48  47303  fourierdlem49  47304  fourierdlem71  47326  fourierdlem81  47336  preimagelt  47848  preimalegt  47849  smfliminflem  47979  smfliminfmpt  47981  chnsubseqwl  48028  fcoresfob  48281  m1mod0mod1  48569  uhgrimedg  49128  isubgr3stgrlem8  49210  rngcinvALTV  49512  ringcinvALTV  49546  prelrrx2bd  49965  xpco2  50107  ovconstbrd  50112  ovconstbrn0d  50113  lubeldm2  50209  glbeldm2  50210  upeu2lem  50281  sectpropd  50290  invpropd  50292  isopropd  50294  cicerALT  50299  cicpropd  50303  up1st2ndb  50442  uobffth  50473  uobeqw  50474  natoppfb  50492  oppc1stflem  50548  fucofulem1  50571  functhinclem1  50718  fullthinc  50724  thincciso4  50731  thinciso  50744  functermclem  50781  termcterm3  50789  termcciso  50790  termcarweu  50802  termfucterm  50821  prstchom2ALT  50841  lanval2  50949  ranval2  50952