Theorem impbida 800

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  822  bibiad  839  eqrdav  2733  eqsndOLD  4785  frsn  5710  funfvbrb  6994  iinpreima  7012  fcdmssb  7065  fnprb  7152  fntpb  7153  fpr2g  7155  nvocnv  7225  fsnex  7227  f1ocnv2d  7609  resf1extb  7874  el2xptp0  7978  1stconst  8040  2ndconst  8041  cnvf1o  8051  fimaproj  8075  tfrlem15  8321  oeeui  8528  ersymb  8647  swoer  8664  erth  8687  boxriin  8876  boxcutc  8877  domunsncan  9003  pw2f1olem  9007  enen1  9043  enen2  9044  domen1  9045  domen2  9046  sdomen1  9047  sdomen2  9048  xpmapenlem  9070  ensymfib  9106  ordiso2  9418  wdomen1  9479  wdomen2  9480  fin23lem26  10233  fpwwe2lem7  10546  r1wunlim  10646  mul2lt0bi  13011  ixxun  13275  xov1plusxeqvd  13412  fzsplit2  13463  fseq1p1m1  13512  elfz2nn0  13532  flflp1  13725  modaddb  13827  modsubdir  13861  zesq  14147  expnngt1b  14163  hashprg  14316  hashgt0elexb  14323  hashbclem  14373  hashge2el2difb  14403  rereb  15041  rlimclim  15467  iserex  15578  caucvgb  15601  mptfzshft  15699  fsumrev  15700  climcnds  15772  fprodrev  15898  dvdsadd2b  16231  nn0ob  16309  bitsfzo  16360  dfgcd2  16471  dvdsmulgcd  16481  lcmgcdeq  16537  qden1elz  16682  mrcidb  17536  mrieqvlemd  17550  isacs2  17574  cicer  17728  ssclem  17741  issubc3  17771  ffthiso  17853  fuciso  17900  setcmon  18009  setcepi  18010  setcinv  18012  catciso  18033  acsfiindd  18474  issstrmgm  18576  mgmhmf1o  18623  issubmgm2  18626  subsubmgm  18633  resmgmhm2b  18636  issubmnd  18684  mhmf1o  18719  subsubm  18739  resmhm2b  18745  grpinvid1  18919  grpinvid2  18920  subsubg  19077  ssnmz  19093  ghmf1  19173  kerf1ghm  19174  ghmf1o  19175  conjnmzb  19180  subggim  19193  gicsubgen  19206  ghmqusnsglem1  19207  ghmquskerlem1  19210  ghmqusker  19214  gass  19228  odf1  19489  gex1  19518  fislw  19552  sylow3lem2  19555  sylow3lem6  19559  lsmdisj2a  19614  lsmdisj2b  19615  efgred2  19680  dmdprdsplit  19976  2nsgsimpgd  20031  simpgnsgbid  20032  ablsimpgd  20045  ogrpinv0le  20063  ogrpaddltbi  20066  ogrpaddltrbid  20068  ogrpinv0lt  20070  0unit  20330  irrednegb  20365  rnghmf1o  20386  rhmf1o  20424  subsubrng  20494  subrgunit  20521  subsubrg  20529  rngcinv  20568  ringcinv  20602  isdrng2  20674  issubdrg  20711  islss3  20908  islss4  20911  ellspsn6  20943  lspsneq0b  20962  islmhm2  20988  lmhmf1o  20996  reslmhm2b  21004  lssvs0or  21063  lvecinv  21066  ellspsn4  21077  lspdisjb  21079  islbs2  21107  islbs3  21108  dflidl2rng  21171  rngringbd  21261  prmirredlem  21425  islindf3  21779  lindsmm  21781  lsslindf  21783  lsslinds  21784  issubassa  21820  sraassab  21821  issubassa2  21846  gsumbagdiag  21885  subrgasclcl  22020  ply1scleq  22247  matunit  22620  slesolinvbi  22623  en2top  22927  elcls  23015  neindisj2  23065  neiptopnei  23074  neiptopreu  23075  maxlp  23089  neitr  23122  iscncl  23211  cncnp  23222  isreg2  23319  dis2ndc  23402  1stccnp  23404  islly2  23426  dislly  23439  dissnlocfin  23471  kgencmp2  23488  pt1hmeo  23748  xkocnv  23756  t0kq  23760  uffixfr  23865  flimcf  23924  cnpflf2  23942  fclscf  23967  cnextf  24008  utopsnneiplem  24189  isucn2  24220  cfilucfil  24501  psmetutop  24509  restmetu  24512  tngngp2  24594  tngngp  24596  nmoleub  24673  metdseq0  24797  cnheibor  24908  pcophtb  24983  nmoleub2lem  25068  lmmbr  25212  iscfil3  25227  cmetss  25270  cldcss  25395  mbfeqalem2  25597  mbfposb  25608  itg2const2  25696  itgss3  25770  plyco0  26151  dgrlt  26226  ulm2  26348  coseq00topi  26465  coseq0negpitopi  26466  sineq0  26487  relogbcxpb  26751  atans2  26895  xrlimcnp  26932  dchrelbas2  27202  dchrn0  27215  2sqb  27397  nosupbnd2  27682  noinfbnd2  27697  slerec  27787  sltmul2  28140  elreno2  28440  istrkg2ld  28481  tgcgreqb  28502  tgbtwncomb  28510  trgcgrg  28536  legov  28606  legov2  28607  legov3  28619  hlbtwn  28632  tglineelsb2  28653  tglinecom  28656  colline  28670  mirinv  28687  mirbtwnb  28693  mirbtwnhl  28701  perpcom  28734  isperp2  28736  oppcom  28765  opphllem3  28770  lnopp2hpgb  28784  colopp  28790  colhp  28791  lmieu  28805  iscgra1  28831  dfcgra2  28851  edgnbusgreu  29389  nb3grprlem1  29402  lfgriswlk  29709  eleclclwwlknlem2  30085  clwwlknscsh  30086  clwwlknon1  30121  numclwwlk2lem1  30400  grpoinvid1  30552  grpoinvid2  30553  leopmul  32158  hst1h  32251  eqelbid  32498  diffib  32545  ifnebib  32573  iinabrex  32593  disjabrex  32606  disjabrexf  32607  erbr3b  32644  f1o3d  32653  funimass4f  32664  2ndimaxp  32673  fgreu  32699  fcnvgreu  32700  1stpreimas  32734  fcobij  32748  cocnvf1o  32757  resf1o  32758  nn0xmulclb  32800  fzsplit3  32822  fzo0opth  32832  sgn3da  32864  sgnnbi  32868  sgnpbi  32869  sgnmulsgn  32872  sgnmulsgp  32873  eliccioo  32961  mgcmntco  33025  dfmgc2lem  33026  dfmgc2  33027  pwrssmgc  33031  mgcf1o  33034  mndlrinvb  33056  mndlactfo  33058  mndractfo  33060  mndlactf1o  33061  mndractf1o  33062  gsumhashmul  33099  gsumwrd2dccatlem  33108  cyc3genpm  33183  isarchi3  33218  prmsimpcyc  33259  elrgspnsubrunlem1  33278  elrgspnsubrun  33280  domnlcanbOLD  33312  isdrng4  33326  fracerl  33337  qsxpid  33392  dvdsruasso  33415  dvdsruasso2  33416  dvdsrspss  33417  grplsmid  33434  quslsm  33435  nsgmgc  33442  nsgqusf1olem2  33444  nsgqusf1olem3  33445  pidlnzb  33452  unitpidl1  33454  elrspunidl  33458  elrspunsn  33459  drngidl  33463  drngidlhash  33464  isprmidlc  33477  prmidl0  33480  qsidom  33484  mxidlirred  33502  mxidlnzrb  33510  qsdrng  33527  rsprprmprmidlb  33553  rprmirredb  33562  deg1le0eq0  33603  ply1unit  33605  evlextv  33656  mplvrpmrhm  33661  esplyfv1  33676  esplyind  33680  lvecdim0  33712  extdg1b  33773  fldextrspunlsp  33780  irngnzply1  33797  1smat1  33910  ist0cld  33939  qtophaus  33942  reff  33945  locfinreflem  33946  cmpcref  33956  zarcls1  33975  zarclsun  33976  zarclsiin  33977  zarclssn  33979  metider  34000  pstmfval  34002  qqhval2  34088  aean  34350  imambfm  34368  eulerpartlemgvv  34482  orvcgteel  34574  orvclteel  34579  ballotlemsf1o  34620  actfunsnf1o  34710  reprsuc  34721  reprpmtf1o  34732  sconnpi1  35382  brofs2  36220  brifs2  36221  broutsideof2  36265  bj-abv  37050  irrdiff  37470  ltflcei  37748  poimirlem25  37785  ismblfin  37801  cnambfre  37808  ftc1anclem6  37838  ismndo1  38013  isdrngo2  38098  eqvrelsymb  38802  eqvrelth  38807  lshpnelb  39183  lshpnel2N  39184  lsatspn0  39199  lsatelbN  39205  lsat0cv  39232  lcvexch  39238  lcv1  39240  lkrshp3  39305  lkrpssN  39362  lkrss2N  39368  cvlsupr2  39542  atcvrlln  39719  llncvrlpln  39757  2llnmj  39759  lplncvrlvol  39815  2lplnmj  39821  polcon2bN  40119  pcl0bN  40122  lhpmcvr3  40224  lhpmatb  40230  ltrncoidN  40327  ltrneq3  40407  ltrniotavalbN  40783  cdlemg1cN  40786  diclspsn  41393  dihopelvalcpre  41447  dihord4  41457  dihord  41463  dihmeetlem4preN  41505  dih1dimatlem0  41527  dochsscl  41567  dochoccl  41568  dochord  41569  dochsat  41582  dochshpncl  41583  dochsatshpb  41651  dochshpsat  41653  mapdval4N  41831  mapdsn  41840  hdmap14lem12  42078  hdmapip0  42114  hlhillcs  42157  resuppsinopn  42560  mulgt0b2d  42675  mullt0b1d  42680  mullt0b2d  42681  riccrng  42719  ricdrng  42726  prjspner1  42811  mrefg2  42891  mzpmfp  42931  lzenom  42954  elpell14qr2  43046  elpell1qr2  43056  pellfund14b  43083  congabseq  43158  acongeq  43167  jm2.23  43180  jm2.20nn  43181  jm2.25lem1  43182  wepwsolem  43226  islssfg2  43255  lnmlmic  43272  dfacbasgrp  43292  unielss  43402  rfovcnvf1od  44187  dssmapnvod  44203  ntrclscls00  44249  rfcnpre3  45220  rfcnpre4  45221  ssmapsn  45402  rnmptssbi  45446  infxrgelbrnmpt  45640  xnegre  45652  xrpnf  45671  rexanuz2nf  45678  ioossioobi  45705  iccshift  45706  iocopn  45708  eliccelioc  45709  iooshift  45710  icoopn  45713  qinioo  45723  limcdm0  45806  islptre  45807  islpcn  45825  limcresioolb  45829  climuzlem  45929  climlimsup  45946  liminfgelimsup  45968  liminfgelimsupuz  45974  climliminf  45992  climliminflimsup  45994  climliminflimsup2  45995  xlimpnfxnegmnf  46000  xlimbr  46013  xlimmnfv  46020  xlimpnfv  46024  xlimclim2  46026  dfxlim2v  46033  climresdm  46036  xlimresdm  46045  xlimliminflimsup  46048  fperdvper  46105  itgperiod  46167  fourierdlem32  46325  fourierdlem33  46326  fourierdlem48  46340  fourierdlem49  46341  fourierdlem71  46363  fourierdlem81  46373  preimagelt  46885  preimalegt  46886  smfliminflem  47016  smfliminfmpt  47018  chnsubseqwl  47065  fcoresfob  47260  m1mod0mod1  47542  uhgrimedg  48079  isubgr3stgrlem8  48161  rngcinvALTV  48464  ringcinvALTV  48498  xpco2  49044  fvconstr  49049  fvconstrn0  49050  lubeldm2  49143  glbeldm2  49144  upeu2lem  49215  sectpropd  49224  invpropd  49226  isopropd  49228  cicerALT  49233  cicpropd  49237  up1st2ndb  49374  uobffth  49405  uobeqw  49406  natoppfb  49418  oppc1stflem  49474  fucofulem1  49497  functhinclem1  49631  fullthinc  49637  thincciso4  49644  thinciso  49657  functermclem  49694  termcterm3  49702  termcciso  49703  termcarweu  49715  termfucterm  49731  prstchom2ALT  49751  lanval2  49814  ranval2  49817