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  2728  eqsndOLD  4782  frsn  5707  funfvbrb  6985  iinpreima  7003  fcdmssb  7056  fnprb  7144  fntpb  7145  fpr2g  7147  nvocnv  7218  fsnex  7220  f1ocnv2d  7602  resf1extb  7867  el2xptp0  7971  1stconst  8033  2ndconst  8034  cnvf1o  8044  fimaproj  8068  tfrlem15  8314  oeeui  8520  ersymb  8639  swoer  8656  erth  8679  boxriin  8867  boxcutc  8868  domunsncan  8994  pw2f1olem  8998  enen1  9034  enen2  9035  domen1  9036  domen2  9037  sdomen1  9038  sdomen2  9039  xpmapenlem  9061  ensymfib  9098  ordiso2  9407  wdomen1  9468  wdomen2  9469  fin23lem26  10219  fpwwe2lem7  10531  r1wunlim  10631  mul2lt0bi  13001  ixxun  13264  xov1plusxeqvd  13401  fzsplit2  13452  fseq1p1m1  13501  elfz2nn0  13521  flflp1  13711  modaddb  13813  modsubdir  13847  zesq  14133  expnngt1b  14149  hashprg  14302  hashgt0elexb  14309  hashbclem  14359  hashge2el2difb  14389  rereb  15027  rlimclim  15453  iserex  15564  caucvgb  15587  mptfzshft  15685  fsumrev  15686  climcnds  15758  fprodrev  15884  dvdsadd2b  16217  nn0ob  16295  bitsfzo  16346  dfgcd2  16457  dvdsmulgcd  16467  lcmgcdeq  16523  qden1elz  16668  mrcidb  17521  mrieqvlemd  17535  isacs2  17559  cicer  17713  ssclem  17726  issubc3  17756  ffthiso  17838  fuciso  17885  setcmon  17994  setcepi  17995  setcinv  17997  catciso  18018  acsfiindd  18459  issstrmgm  18527  mgmhmf1o  18574  issubmgm2  18577  subsubmgm  18584  resmgmhm2b  18587  issubmnd  18635  mhmf1o  18670  subsubm  18690  resmhm2b  18696  grpinvid1  18870  grpinvid2  18871  subsubg  19028  ssnmz  19045  ghmf1  19125  kerf1ghm  19126  ghmf1o  19127  conjnmzb  19132  subggim  19145  gicsubgen  19158  ghmqusnsglem1  19159  ghmquskerlem1  19162  ghmqusker  19166  gass  19180  odf1  19441  gex1  19470  fislw  19504  sylow3lem2  19507  sylow3lem6  19511  lsmdisj2a  19566  lsmdisj2b  19567  efgred2  19632  dmdprdsplit  19928  2nsgsimpgd  19983  simpgnsgbid  19984  ablsimpgd  19997  ogrpinv0le  20015  ogrpaddltbi  20018  ogrpaddltrbid  20020  ogrpinv0lt  20022  0unit  20281  irrednegb  20316  rnghmf1o  20337  rhmf1o  20376  subsubrng  20448  subrgunit  20475  subsubrg  20483  rngcinv  20522  ringcinv  20556  isdrng2  20628  issubdrg  20665  islss3  20862  islss4  20865  ellspsn6  20897  lspsneq0b  20916  islmhm2  20942  lmhmf1o  20950  reslmhm2b  20958  lssvs0or  21017  lvecinv  21020  ellspsn4  21031  lspdisjb  21033  islbs2  21061  islbs3  21062  dflidl2rng  21125  rngringbd  21215  prmirredlem  21379  islindf3  21733  lindsmm  21735  lsslindf  21737  lsslinds  21738  issubassa  21774  sraassab  21775  issubassa2  21799  gsumbagdiag  21838  subrgasclcl  21972  ply1scleq  22190  matunit  22563  slesolinvbi  22566  en2top  22870  elcls  22958  neindisj2  23008  neiptopnei  23017  neiptopreu  23018  maxlp  23032  neitr  23065  iscncl  23154  cncnp  23165  isreg2  23262  dis2ndc  23345  1stccnp  23347  islly2  23369  dislly  23382  dissnlocfin  23414  kgencmp2  23431  pt1hmeo  23691  xkocnv  23699  t0kq  23703  uffixfr  23808  flimcf  23867  cnpflf2  23885  fclscf  23910  cnextf  23951  utopsnneiplem  24133  isucn2  24164  cfilucfil  24445  psmetutop  24453  restmetu  24456  tngngp2  24538  tngngp  24540  nmoleub  24617  metdseq0  24741  cnheibor  24852  pcophtb  24927  nmoleub2lem  25012  lmmbr  25156  iscfil3  25171  cmetss  25214  cldcss  25339  mbfeqalem2  25541  mbfposb  25552  itg2const2  25640  itgss3  25714  plyco0  26095  dgrlt  26170  ulm2  26292  coseq00topi  26409  coseq0negpitopi  26410  sineq0  26431  relogbcxpb  26695  atans2  26839  xrlimcnp  26876  dchrelbas2  27146  dchrn0  27159  2sqb  27341  nosupbnd2  27626  noinfbnd2  27641  slerec  27730  sltmul2  28079  istrkg2ld  28405  tgcgreqb  28426  tgbtwncomb  28434  trgcgrg  28460  legov  28530  legov2  28531  legov3  28543  hlbtwn  28556  tglineelsb2  28577  tglinecom  28580  colline  28594  mirinv  28611  mirbtwnb  28617  mirbtwnhl  28625  perpcom  28658  isperp2  28660  oppcom  28689  opphllem3  28694  lnopp2hpgb  28708  colopp  28714  colhp  28715  lmieu  28729  iscgra1  28755  dfcgra2  28775  edgnbusgreu  29312  nb3grprlem1  29325  lfgriswlk  29632  eleclclwwlknlem2  30005  clwwlknscsh  30006  clwwlknon1  30041  numclwwlk2lem1  30320  grpoinvid1  30472  grpoinvid2  30473  leopmul  32078  hst1h  32171  eqelbid  32419  diffib  32465  ifnebib  32493  iinabrex  32513  disjabrex  32526  disjabrexf  32527  erbr3b  32562  f1o3d  32569  funimass4f  32580  2ndimaxp  32589  fgreu  32615  fcnvgreu  32616  1stpreimas  32648  fcobij  32664  resf1o  32673  nn0xmulclb  32714  fzsplit3  32736  fzo0opth  32748  sgn3da  32779  sgnnbi  32783  sgnpbi  32784  sgnmulsgn  32787  sgnmulsgp  32788  eliccioo  32871  mgcmntco  32936  dfmgc2lem  32937  dfmgc2  32938  pwrssmgc  32942  mgcf1o  32945  mndlrinvb  32979  mndlactfo  32981  mndractfo  32983  mndlactf1o  32984  mndractf1o  32985  gsumhashmul  33014  gsumwrd2dccatlem  33019  cyc3genpm  33094  isarchi3  33129  prmsimpcyc  33170  elrgspnsubrunlem1  33187  elrgspnsubrun  33189  domnlcanbOLD  33220  isdrng4  33234  fracerl  33245  qsxpid  33299  dvdsruasso  33322  dvdsruasso2  33323  dvdsrspss  33324  grplsmid  33341  quslsm  33342  nsgmgc  33349  nsgqusf1olem2  33351  nsgqusf1olem3  33352  pidlnzb  33359  unitpidl1  33361  elrspunidl  33365  elrspunsn  33366  drngidl  33370  drngidlhash  33371  isprmidlc  33384  prmidl0  33387  qsidom  33391  mxidlirred  33409  mxidlnzrb  33417  qsdrng  33434  rsprprmprmidlb  33460  rprmirredb  33469  deg1le0eq0  33508  ply1unit  33510  lvecdim0  33573  extdg1b  33634  fldextrspunlsp  33641  irngnzply1  33658  1smat1  33771  ist0cld  33800  qtophaus  33803  reff  33806  locfinreflem  33807  cmpcref  33817  zarcls1  33836  zarclsun  33837  zarclsiin  33838  zarclssn  33840  metider  33861  pstmfval  33863  qqhval2  33949  aean  34211  imambfm  34230  eulerpartlemgvv  34344  orvcgteel  34436  orvclteel  34441  ballotlemsf1o  34482  actfunsnf1o  34572  reprsuc  34583  reprpmtf1o  34594  sconnpi1  35216  brofs2  36055  brifs2  36056  broutsideof2  36100  bj-abv  36884  irrdiff  37304  ltflcei  37592  poimirlem25  37629  ismblfin  37645  cnambfre  37652  ftc1anclem6  37682  ismndo1  37857  isdrngo2  37942  eqvrelsymb  38587  eqvrelth  38592  lshpnelb  38967  lshpnel2N  38968  lsatspn0  38983  lsatelbN  38989  lsat0cv  39016  lcvexch  39022  lcv1  39024  lkrshp3  39089  lkrpssN  39146  lkrss2N  39152  cvlsupr2  39326  atcvrlln  39503  llncvrlpln  39541  2llnmj  39543  lplncvrlvol  39599  2lplnmj  39605  polcon2bN  39903  pcl0bN  39906  lhpmcvr3  40008  lhpmatb  40014  ltrncoidN  40111  ltrneq3  40191  ltrniotavalbN  40567  cdlemg1cN  40570  diclspsn  41177  dihopelvalcpre  41231  dihord4  41241  dihord  41247  dihmeetlem4preN  41289  dih1dimatlem0  41311  dochsscl  41351  dochoccl  41352  dochord  41353  dochsat  41366  dochshpncl  41367  dochsatshpb  41435  dochshpsat  41437  mapdval4N  41615  mapdsn  41624  hdmap14lem12  41862  hdmapip0  41898  hlhillcs  41941  resuppsinopn  42340  mulgt0b2d  42455  mullt0b1d  42460  mullt0b2d  42461  riccrng  42499  ricdrng  42506  prjspner1  42603  mrefg2  42684  mzpmfp  42724  lzenom  42747  elpell14qr2  42839  elpell1qr2  42849  pellfund14b  42876  congabseq  42951  acongeq  42960  jm2.23  42973  jm2.20nn  42974  jm2.25lem1  42975  wepwsolem  43019  islssfg2  43048  lnmlmic  43065  dfacbasgrp  43085  unielss  43195  rfovcnvf1od  43981  dssmapnvod  43997  ntrclscls00  44043  rfcnpre3  45015  rfcnpre4  45016  ssmapsn  45198  rnmptssbi  45242  infxrgelbrnmpt  45437  xnegre  45449  xrpnf  45468  rexanuz2nf  45475  ioossioobi  45502  iccshift  45503  iocopn  45505  eliccelioc  45506  iooshift  45507  icoopn  45510  qinioo  45520  limcdm0  45603  islptre  45604  islpcn  45624  limcresioolb  45628  climuzlem  45728  climlimsup  45745  liminfgelimsup  45767  liminfgelimsupuz  45773  climliminf  45791  climliminflimsup  45793  climliminflimsup2  45794  xlimpnfxnegmnf  45799  xlimbr  45812  xlimmnfv  45819  xlimpnfv  45823  xlimclim2  45825  dfxlim2v  45832  climresdm  45835  xlimresdm  45844  xlimliminflimsup  45847  fperdvper  45904  itgperiod  45966  fourierdlem32  46124  fourierdlem33  46125  fourierdlem48  46139  fourierdlem49  46140  fourierdlem71  46162  fourierdlem81  46172  preimagelt  46684  preimalegt  46685  smfliminflem  46815  smfliminfmpt  46817  fcoresfob  47060  m1mod0mod1  47342  uhgrimedg  47879  isubgr3stgrlem8  47961  rngcinvALTV  48264  ringcinvALTV  48298  xpco2  48845  fvconstr  48850  fvconstrn0  48851  lubeldm2  48944  glbeldm2  48945  upeu2lem  49017  sectpropd  49026  invpropd  49028  isopropd  49030  cicerALT  49035  cicpropd  49039  up1st2ndb  49176  uobffth  49207  uobeqw  49208  natoppfb  49220  oppc1stflem  49276  fucofulem1  49299  functhinclem1  49433  fullthinc  49439  thincciso4  49446  thinciso  49459  functermclem  49496  termcterm3  49504  termcciso  49505  termcarweu  49517  termfucterm  49533  prstchom2ALT  49553  lanval2  49616  ranval2  49619