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  2730  eqsndOLD  4780  frsn  5702  funfvbrb  6984  iinpreima  7002  fcdmssb  7055  fnprb  7142  fntpb  7143  fpr2g  7145  nvocnv  7215  fsnex  7217  f1ocnv2d  7599  resf1extb  7864  el2xptp0  7968  1stconst  8030  2ndconst  8031  cnvf1o  8041  fimaproj  8065  tfrlem15  8311  oeeui  8517  ersymb  8636  swoer  8653  erth  8676  boxriin  8864  boxcutc  8865  domunsncan  8990  pw2f1olem  8994  enen1  9030  enen2  9031  domen1  9032  domen2  9033  sdomen1  9034  sdomen2  9035  xpmapenlem  9057  ensymfib  9093  ordiso2  9401  wdomen1  9462  wdomen2  9463  fin23lem26  10216  fpwwe2lem7  10528  r1wunlim  10628  mul2lt0bi  12998  ixxun  13261  xov1plusxeqvd  13398  fzsplit2  13449  fseq1p1m1  13498  elfz2nn0  13518  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  18561  mgmhmf1o  18608  issubmgm2  18611  subsubmgm  18618  resmgmhm2b  18621  issubmnd  18669  mhmf1o  18704  subsubm  18724  resmhm2b  18730  grpinvid1  18904  grpinvid2  18905  subsubg  19062  ssnmz  19078  ghmf1  19158  kerf1ghm  19159  ghmf1o  19160  conjnmzb  19165  subggim  19178  gicsubgen  19191  ghmqusnsglem1  19192  ghmquskerlem1  19195  ghmqusker  19199  gass  19213  odf1  19474  gex1  19503  fislw  19537  sylow3lem2  19540  sylow3lem6  19544  lsmdisj2a  19599  lsmdisj2b  19600  efgred2  19665  dmdprdsplit  19961  2nsgsimpgd  20016  simpgnsgbid  20017  ablsimpgd  20030  ogrpinv0le  20048  ogrpaddltbi  20051  ogrpaddltrbid  20053  ogrpinv0lt  20055  0unit  20314  irrednegb  20349  rnghmf1o  20370  rhmf1o  20408  subsubrng  20478  subrgunit  20505  subsubrg  20513  rngcinv  20552  ringcinv  20586  isdrng2  20658  issubdrg  20695  islss3  20892  islss4  20895  ellspsn6  20927  lspsneq0b  20946  islmhm2  20972  lmhmf1o  20980  reslmhm2b  20988  lssvs0or  21047  lvecinv  21050  ellspsn4  21061  lspdisjb  21063  islbs2  21091  islbs3  21092  dflidl2rng  21155  rngringbd  21245  prmirredlem  21409  islindf3  21763  lindsmm  21765  lsslindf  21767  lsslinds  21768  issubassa  21804  sraassab  21805  issubassa2  21829  gsumbagdiag  21868  subrgasclcl  22002  ply1scleq  22220  matunit  22593  slesolinvbi  22596  en2top  22900  elcls  22988  neindisj2  23038  neiptopnei  23047  neiptopreu  23048  maxlp  23062  neitr  23095  iscncl  23184  cncnp  23195  isreg2  23292  dis2ndc  23375  1stccnp  23377  islly2  23399  dislly  23412  dissnlocfin  23444  kgencmp2  23461  pt1hmeo  23721  xkocnv  23729  t0kq  23733  uffixfr  23838  flimcf  23897  cnpflf2  23915  fclscf  23940  cnextf  23981  utopsnneiplem  24162  isucn2  24193  cfilucfil  24474  psmetutop  24482  restmetu  24485  tngngp2  24567  tngngp  24569  nmoleub  24646  metdseq0  24770  cnheibor  24881  pcophtb  24956  nmoleub2lem  25041  lmmbr  25185  iscfil3  25200  cmetss  25243  cldcss  25368  mbfeqalem2  25570  mbfposb  25581  itg2const2  25669  itgss3  25743  plyco0  26124  dgrlt  26199  ulm2  26321  coseq00topi  26438  coseq0negpitopi  26439  sineq0  26460  relogbcxpb  26724  atans2  26868  xrlimcnp  26905  dchrelbas2  27175  dchrn0  27188  2sqb  27370  nosupbnd2  27655  noinfbnd2  27670  slerec  27760  sltmul2  28110  istrkg2ld  28438  tgcgreqb  28459  tgbtwncomb  28467  trgcgrg  28493  legov  28563  legov2  28564  legov3  28576  hlbtwn  28589  tglineelsb2  28610  tglinecom  28613  colline  28627  mirinv  28644  mirbtwnb  28650  mirbtwnhl  28658  perpcom  28691  isperp2  28693  oppcom  28722  opphllem3  28727  lnopp2hpgb  28741  colopp  28747  colhp  28748  lmieu  28762  iscgra1  28788  dfcgra2  28808  edgnbusgreu  29345  nb3grprlem1  29358  lfgriswlk  29665  eleclclwwlknlem2  30041  clwwlknscsh  30042  clwwlknon1  30077  numclwwlk2lem1  30356  grpoinvid1  30508  grpoinvid2  30509  leopmul  32114  hst1h  32207  eqelbid  32454  diffib  32501  ifnebib  32529  iinabrex  32549  disjabrex  32562  disjabrexf  32563  erbr3b  32600  f1o3d  32608  funimass4f  32619  2ndimaxp  32628  fgreu  32654  fcnvgreu  32655  1stpreimas  32687  fcobij  32703  cocnvf1o  32712  resf1o  32713  nn0xmulclb  32754  fzsplit3  32776  fzo0opth  32785  sgn3da  32817  sgnnbi  32821  sgnpbi  32822  sgnmulsgn  32825  sgnmulsgp  32826  eliccioo  32911  mgcmntco  32975  dfmgc2lem  32976  dfmgc2  32977  pwrssmgc  32981  mgcf1o  32984  mndlrinvb  33006  mndlactfo  33008  mndractfo  33010  mndlactf1o  33011  mndractf1o  33012  gsumhashmul  33041  gsumwrd2dccatlem  33046  cyc3genpm  33121  isarchi3  33156  prmsimpcyc  33197  elrgspnsubrunlem1  33214  elrgspnsubrun  33216  domnlcanbOLD  33247  isdrng4  33261  fracerl  33272  qsxpid  33327  dvdsruasso  33350  dvdsruasso2  33351  dvdsrspss  33352  grplsmid  33369  quslsm  33370  nsgmgc  33377  nsgqusf1olem2  33379  nsgqusf1olem3  33380  pidlnzb  33387  unitpidl1  33389  elrspunidl  33393  elrspunsn  33394  drngidl  33398  drngidlhash  33399  isprmidlc  33412  prmidl0  33415  qsidom  33419  mxidlirred  33437  mxidlnzrb  33445  qsdrng  33462  rsprprmprmidlb  33488  rprmirredb  33497  deg1le0eq0  33536  ply1unit  33538  mplvrpmrhm  33577  esplyfv1  33590  lvecdim0  33619  extdg1b  33680  fldextrspunlsp  33687  irngnzply1  33704  1smat1  33817  ist0cld  33846  qtophaus  33849  reff  33852  locfinreflem  33853  cmpcref  33863  zarcls1  33882  zarclsun  33883  zarclsiin  33884  zarclssn  33886  metider  33907  pstmfval  33909  qqhval2  33995  aean  34257  imambfm  34275  eulerpartlemgvv  34389  orvcgteel  34481  orvclteel  34486  ballotlemsf1o  34527  actfunsnf1o  34617  reprsuc  34628  reprpmtf1o  34639  sconnpi1  35283  brofs2  36121  brifs2  36122  broutsideof2  36166  bj-abv  36950  irrdiff  37370  ltflcei  37658  poimirlem25  37695  ismblfin  37711  cnambfre  37718  ftc1anclem6  37748  ismndo1  37923  isdrngo2  38008  eqvrelsymb  38712  eqvrelth  38717  lshpnelb  39093  lshpnel2N  39094  lsatspn0  39109  lsatelbN  39115  lsat0cv  39142  lcvexch  39148  lcv1  39150  lkrshp3  39215  lkrpssN  39272  lkrss2N  39278  cvlsupr2  39452  atcvrlln  39629  llncvrlpln  39667  2llnmj  39669  lplncvrlvol  39725  2lplnmj  39731  polcon2bN  40029  pcl0bN  40032  lhpmcvr3  40134  lhpmatb  40140  ltrncoidN  40237  ltrneq3  40317  ltrniotavalbN  40693  cdlemg1cN  40696  diclspsn  41303  dihopelvalcpre  41357  dihord4  41367  dihord  41373  dihmeetlem4preN  41415  dih1dimatlem0  41437  dochsscl  41477  dochoccl  41478  dochord  41479  dochsat  41492  dochshpncl  41493  dochsatshpb  41561  dochshpsat  41563  mapdval4N  41741  mapdsn  41750  hdmap14lem12  41988  hdmapip0  42024  hlhillcs  42067  resuppsinopn  42466  mulgt0b2d  42581  mullt0b1d  42586  mullt0b2d  42587  riccrng  42625  ricdrng  42632  prjspner1  42729  mrefg2  42810  mzpmfp  42850  lzenom  42873  elpell14qr2  42965  elpell1qr2  42975  pellfund14b  43002  congabseq  43077  acongeq  43086  jm2.23  43099  jm2.20nn  43100  jm2.25lem1  43101  wepwsolem  43145  islssfg2  43174  lnmlmic  43191  dfacbasgrp  43211  unielss  43321  rfovcnvf1od  44107  dssmapnvod  44123  ntrclscls00  44169  rfcnpre3  45140  rfcnpre4  45141  ssmapsn  45323  rnmptssbi  45367  infxrgelbrnmpt  45562  xnegre  45574  xrpnf  45593  rexanuz2nf  45600  ioossioobi  45627  iccshift  45628  iocopn  45630  eliccelioc  45631  iooshift  45632  icoopn  45635  qinioo  45645  limcdm0  45728  islptre  45729  islpcn  45747  limcresioolb  45751  climuzlem  45851  climlimsup  45868  liminfgelimsup  45890  liminfgelimsupuz  45896  climliminf  45914  climliminflimsup  45916  climliminflimsup2  45917  xlimpnfxnegmnf  45922  xlimbr  45935  xlimmnfv  45942  xlimpnfv  45946  xlimclim2  45948  dfxlim2v  45955  climresdm  45958  xlimresdm  45967  xlimliminflimsup  45970  fperdvper  46027  itgperiod  46089  fourierdlem32  46247  fourierdlem33  46248  fourierdlem48  46262  fourierdlem49  46263  fourierdlem71  46285  fourierdlem81  46295  preimagelt  46807  preimalegt  46808  smfliminflem  46938  smfliminfmpt  46940  chnsubseqwl  46987  fcoresfob  47182  m1mod0mod1  47464  uhgrimedg  48001  isubgr3stgrlem8  48083  rngcinvALTV  48386  ringcinvALTV  48420  xpco2  48967  fvconstr  48972  fvconstrn0  48973  lubeldm2  49066  glbeldm2  49067  upeu2lem  49139  sectpropd  49148  invpropd  49150  isopropd  49152  cicerALT  49157  cicpropd  49161  up1st2ndb  49298  uobffth  49329  uobeqw  49330  natoppfb  49342  oppc1stflem  49398  fucofulem1  49421  functhinclem1  49555  fullthinc  49561  thincciso4  49568  thinciso  49581  functermclem  49618  termcterm3  49626  termcciso  49627  termcarweu  49639  termfucterm  49655  prstchom2ALT  49675  lanval2  49738  ranval2  49741