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  4813  frsn  5755  funfvbrb  7052  iinpreima  7070  fcdmssb  7123  fnprb  7211  fntpb  7212  fpr2g  7214  nvocnv  7284  fsnex  7286  f1ocnv2d  7669  resf1extb  7939  el2xptp0  8044  1stconst  8108  2ndconst  8109  cnvf1o  8119  fimaproj  8143  tfrlem15  8415  oeeui  8623  ersymb  8742  swoer  8759  erth  8779  boxriin  8963  boxcutc  8964  domunsncan  9095  pw2f1olem  9099  enen1  9140  enen2  9141  domen1  9142  domen2  9143  sdomen1  9144  sdomen2  9145  xpmapenlem  9167  ensymfib  9207  ordiso2  9538  wdomen1  9599  wdomen2  9600  fin23lem26  10348  fpwwe2lem7  10660  r1wunlim  10760  mul2lt0bi  13124  ixxun  13386  xov1plusxeqvd  13521  fzsplit2  13572  fseq1p1m1  13621  elfz2nn0  13641  flflp1  13830  modsubdir  13964  zesq  14248  expnngt1b  14264  hashprg  14417  hashgt0elexb  14424  hashbclem  14474  hashge2el2difb  14504  rereb  15142  rlimclim  15565  iserex  15676  caucvgb  15699  mptfzshft  15797  fsumrev  15798  climcnds  15870  fprodrev  15996  dvdsadd2b  16326  nn0ob  16404  bitsfzo  16455  dfgcd2  16566  dvdsmulgcd  16576  lcmgcdeq  16632  qden1elz  16777  mrcidb  17634  mrieqvlemd  17648  isacs2  17672  cicer  17826  ssclem  17839  issubc3  17870  ffthiso  17952  fuciso  17999  setcmon  18108  setcepi  18109  setcinv  18111  catciso  18132  acsfiindd  18572  issstrmgm  18640  mgmhmf1o  18687  issubmgm2  18690  subsubmgm  18697  resmgmhm2b  18700  issubmnd  18748  mhmf1o  18783  subsubm  18803  resmhm2b  18809  grpinvid1  18983  grpinvid2  18984  subsubg  19141  ssnmz  19158  ghmf1  19238  kerf1ghm  19239  ghmf1o  19240  conjnmzb  19245  subggim  19258  gicsubgen  19271  ghmqusnsglem1  19272  ghmquskerlem1  19275  ghmqusker  19279  gass  19293  odf1  19553  gex1  19582  fislw  19616  sylow3lem2  19619  sylow3lem6  19623  lsmdisj2a  19678  lsmdisj2b  19679  efgred2  19744  dmdprdsplit  20040  2nsgsimpgd  20095  simpgnsgbid  20096  ablsimpgd  20109  0unit  20369  irrednegb  20404  rnghmf1o  20425  rhmf1o  20464  subsubrng  20536  subrgunit  20563  subsubrg  20571  rngcinv  20610  ringcinv  20644  isdrng2  20716  issubdrg  20754  islss3  20930  islss4  20933  ellspsn6  20965  lspsneq0b  20984  islmhm2  21010  lmhmf1o  21018  reslmhm2b  21026  lssvs0or  21085  lvecinv  21088  ellspsn4  21099  lspdisjb  21101  islbs2  21129  islbs3  21130  dflidl2rng  21195  rngringbd  21285  prmirredlem  21450  islindf3  21813  lindsmm  21815  lsslindf  21817  lsslinds  21818  issubassa  21854  sraassab  21855  issubassa2  21879  gsumbagdiag  21918  subrgasclcl  22058  ply1scleq  22276  matunit  22651  slesolinvbi  22654  en2top  22958  elcls  23046  neindisj2  23096  neiptopnei  23105  neiptopreu  23106  maxlp  23120  neitr  23153  iscncl  23242  cncnp  23253  isreg2  23350  dis2ndc  23433  1stccnp  23435  islly2  23457  dislly  23470  dissnlocfin  23502  kgencmp2  23519  pt1hmeo  23779  xkocnv  23787  t0kq  23791  uffixfr  23896  flimcf  23955  cnpflf2  23973  fclscf  23998  cnextf  24039  utopsnneiplem  24221  isucn2  24252  cfilucfil  24535  psmetutop  24543  restmetu  24546  tngngp2  24628  tngngp  24630  nmoleub  24707  metdseq0  24831  cnheibor  24942  pcophtb  25017  nmoleub2lem  25102  lmmbr  25247  iscfil3  25262  cmetss  25305  cldcss  25430  mbfeqalem2  25632  mbfposb  25643  itg2const2  25731  itgss3  25805  plyco0  26186  dgrlt  26261  ulm2  26383  coseq00topi  26499  coseq0negpitopi  26500  sineq0  26521  relogbcxpb  26785  atans2  26929  xrlimcnp  26966  dchrelbas2  27236  dchrn0  27249  2sqb  27431  nosupbnd2  27716  noinfbnd2  27731  slerec  27819  sltmul2  28152  istrkg2ld  28423  tgcgreqb  28444  tgbtwncomb  28452  trgcgrg  28478  legov  28548  legov2  28549  legov3  28561  hlbtwn  28574  tglineelsb2  28595  tglinecom  28598  colline  28612  mirinv  28629  mirbtwnb  28635  mirbtwnhl  28643  perpcom  28676  isperp2  28678  oppcom  28707  opphllem3  28712  lnopp2hpgb  28726  colopp  28732  colhp  28733  lmieu  28747  iscgra1  28773  dfcgra2  28793  edgnbusgreu  29331  nb3grprlem1  29344  lfgriswlk  29653  eleclclwwlknlem2  30027  clwwlknscsh  30028  clwwlknon1  30063  numclwwlk2lem1  30342  grpoinvid1  30494  grpoinvid2  30495  leopmul  32100  hst1h  32193  eqelbid  32441  diffib  32487  ifnebib  32509  iinabrex  32529  disjabrex  32542  disjabrexf  32543  erbr3b  32576  f1o3d  32584  funimass4f  32594  2ndimaxp  32603  fgreu  32629  fcnvgreu  32630  1stpreimas  32662  fcobij  32680  resf1o  32688  nn0xmulclb  32722  fzsplit3  32742  fzo0opth  32754  eliccioo  32860  mgcmntco  32930  dfmgc2lem  32931  dfmgc2  32932  pwrssmgc  32936  mgcf1o  32939  mndlrinvb  32976  mndlactfo  32978  mndractfo  32980  mndlactf1o  32981  mndractf1o  32982  gsumhashmul  33010  gsumwrd2dccatlem  33015  ogrpinv0le  33038  ogrpaddltbi  33041  ogrpaddltrbid  33043  ogrpinv0lt  33045  cyc3genpm  33118  isarchi3  33140  prmsimpcyc  33180  elrgspnsubrunlem1  33197  elrgspnsubrun  33199  domnlcanbOLD  33230  isdrng4  33244  fracerl  33254  qsxpid  33331  dvdsruasso  33354  dvdsruasso2  33355  dvdsrspss  33356  grplsmid  33373  quslsm  33374  nsgmgc  33381  nsgqusf1olem2  33383  nsgqusf1olem3  33384  pidlnzb  33391  unitpidl1  33393  elrspunidl  33397  elrspunsn  33398  drngidl  33402  drngidlhash  33403  isprmidlc  33416  prmidl0  33419  qsidom  33423  mxidlirred  33441  mxidlnzrb  33449  qsdrng  33466  rsprprmprmidlb  33492  rprmirredb  33501  deg1le0eq0  33539  ply1unit  33541  lvecdim0  33598  extdg1b  33658  fldextrspunlsp  33665  irngnzply1  33682  1smat1  33744  ist0cld  33773  qtophaus  33776  reff  33779  locfinreflem  33780  cmpcref  33790  zarcls1  33809  zarclsun  33810  zarclsiin  33811  zarclssn  33813  metider  33834  pstmfval  33836  qqhval2  33924  aean  34186  imambfm  34205  eulerpartlemgvv  34319  orvcgteel  34411  orvclteel  34416  ballotlemsf1o  34457  sgn3da  34485  sgnnbi  34489  sgnpbi  34490  sgnmulsgn  34493  sgnmulsgp  34494  actfunsnf1o  34560  reprsuc  34571  reprpmtf1o  34582  sconnpi1  35185  brofs2  36019  brifs2  36020  broutsideof2  36064  bj-abv  36848  irrdiff  37268  ltflcei  37556  poimirlem25  37593  ismblfin  37609  cnambfre  37616  ftc1anclem6  37646  ismndo1  37821  isdrngo2  37906  eqvrelsymb  38548  eqvrelth  38553  lshpnelb  38926  lshpnel2N  38927  lsatspn0  38942  lsatelbN  38948  lsat0cv  38975  lcvexch  38981  lcv1  38983  lkrshp3  39048  lkrpssN  39105  lkrss2N  39111  cvlsupr2  39285  atcvrlln  39463  llncvrlpln  39501  2llnmj  39503  lplncvrlvol  39559  2lplnmj  39565  polcon2bN  39863  pcl0bN  39866  lhpmcvr3  39968  lhpmatb  39974  ltrncoidN  40071  ltrneq3  40151  ltrniotavalbN  40527  cdlemg1cN  40530  diclspsn  41137  dihopelvalcpre  41191  dihord4  41201  dihord  41207  dihmeetlem4preN  41249  dih1dimatlem0  41271  dochsscl  41311  dochoccl  41312  dochord  41313  dochsat  41326  dochshpncl  41327  dochsatshpb  41395  dochshpsat  41397  mapdval4N  41575  mapdsn  41584  hdmap14lem12  41822  hdmapip0  41858  hlhillcs  41905  resuppsinopn  42338  riccrng  42477  ricdrng  42484  prjspner1  42581  mrefg2  42663  mzpmfp  42703  lzenom  42726  elpell14qr2  42818  elpell1qr2  42828  pellfund14b  42855  congabseq  42931  acongeq  42940  jm2.23  42953  jm2.20nn  42954  jm2.25lem1  42955  wepwsolem  42999  islssfg2  43028  lnmlmic  43045  dfacbasgrp  43065  unielss  43175  rfovcnvf1od  43962  dssmapnvod  43978  ntrclscls00  44024  rfcnpre3  44983  rfcnpre4  44984  ssmapsn  45166  rnmptssbi  45212  infxrgelbrnmpt  45410  xnegre  45422  xrpnf  45441  rexanuz2nf  45448  ioossioobi  45475  iccshift  45476  iocopn  45478  eliccelioc  45479  iooshift  45480  icoopn  45483  qinioo  45493  limcdm0  45578  islptre  45579  islpcn  45599  limcresioolb  45603  climuzlem  45703  climlimsup  45720  liminfgelimsup  45742  liminfgelimsupuz  45748  climliminf  45766  climliminflimsup  45768  climliminflimsup2  45769  xlimpnfxnegmnf  45774  xlimbr  45787  xlimmnfv  45794  xlimpnfv  45798  xlimclim2  45800  dfxlim2v  45807  climresdm  45810  xlimresdm  45819  xlimliminflimsup  45822  fperdvper  45879  itgperiod  45941  fourierdlem32  46099  fourierdlem33  46100  fourierdlem48  46114  fourierdlem49  46115  fourierdlem71  46137  fourierdlem81  46147  preimagelt  46659  preimalegt  46660  smfliminflem  46790  smfliminfmpt  46792  fcoresfob  47030  m1mod0mod1  47302  uspgrimprop  47819  isubgr3stgrlem8  47886  rngcinvALTV  48138  ringcinvALTV  48172  fvconstr  48711  fvconstrn0  48712  lubeldm2  48801  glbeldm2  48802  upeu2lem  48867  fucofulem1  48969  functhinclem1  49059  fullthinc  49065  thincciso4  49072  thinciso  49083  functermclem  49108  termcterm3  49116  termcarweu  49127  prstchom2ALT  49157