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  7044  iinpreima  7063  fcdmssb  7116  fnprb  7208  fntpb  7209  fpr2g  7211  nvocnv  7283  fsnex  7285  f1ocnv2d  7668  resf1extb  7932  el2xptp0  8034  1stconst  8098  2ndconst  8099  cnvf1o  8109  fimaproj  8134  tfrlem15  8382  oeeui  8593  ersymb  8714  swoer  8731  erth  8754  boxriin  8950  boxcutc  8951  domunsncan  9078  pw2f1olem  9082  enen1  9118  enen2  9119  domen1  9120  domen2  9121  sdomen1  9122  sdomen2  9123  xpmapenlem  9145  ensymfib  9181  ordiso2  9490  wdomen1  9551  wdomen2  9552  fin23lem26  10330  fpwwe2lem7  10649  r1wunlim  10749  mul2lt0bi  13153  ixxun  13417  xov1plusxeqvd  13554  fzsplit2  13607  fseq1p1m1  13656  elfz2nn0  13676  flflp1  13871  modaddb  13973  modsubdir  14007  zesq  14293  expnngt1b  14309  hashprg  14462  hashgt0elexb  14469  hashbclem  14520  hashge2el2difb  14550  sgn3da  15177  sgnnbi  15180  sgnpbi  15181  sgnmulsgn  15185  rereb  15210  rlimclim  15636  iserex  15747  caucvgb  15770  mptfzshft  15867  fsumrev  15868  climcnds  15943  fprodrev  16067  dvdsadd2b  16399  nn0ob  16477  bitsfzo  16528  dfgcd2  16639  dvdsmulgcd  16649  lcmgcdeq  16705  qden1elz  16851  mrcidb  17706  mrieqvlemd  17720  isacs2  17744  cicer  17898  ssclem  17911  issubc3  17941  ffthiso  18023  fuciso  18070  setcmon  18179  setcepi  18180  setcinv  18182  catciso  18203  acsfiindd  18644  issstrmgm  18748  mgmhmf1o  18805  issubmgm2  18808  subsubmgm  18815  resmgmhm2b  18818  issubmnd  18869  mhmf1o  18907  subsubm  18928  resmhm2b  18934  grpinvid1  19118  grpinvid2  19119  subsubg  19276  ssnmz  19292  qsxpid  19303  ghmf1  19376  kerf1ghm  19377  ghmf1o  19378  conjnmzb  19383  subggim  19396  gicsubgen  19409  ghmqusnsglem1  19410  ghmquskerlem1  19413  ghmqusker  19417  gass  19431  odf1  19692  gex1  19721  fislw  19755  sylow3lem2  19758  sylow3lem6  19762  lsmdisj2a  19817  lsmdisj2b  19818  efgred2  19883  dmdprdsplit  20179  2nsgsimpgd  20234  simpgnsgbid  20235  ablsimpgd  20248  ogrpinv0le  20266  ogrpaddltbi  20269  ogrpaddltrbid  20271  ogrpinv0lt  20273  0unit  20540  irrednegb  20575  rnghmf1o  20596  rhmf1o  20641  subsubrng  20728  subrgunit  20755  subsubrg  20763  rngcinv  20802  ringcinv  20836  isdrng4  20905  isdrng2  20909  isdrng3  20919  issubdrg  20949  islss3  21146  islss4  21149  ellspsn6  21181  lspsneq0b  21200  islmhm2  21225  lmhmf1o  21233  reslmhm2b  21241  lssvs0or  21300  lvecinv  21303  ellspsn4  21314  lspdisjb  21316  islbs2  21344  islbs3  21345  dflidl2rng  21409  drngidl  21451  rngringbd  21514  isprmidlc  21538  prmidl0  21544  qsidom  21548  prmirredlem  21688  islindf3  22042  lindsmm  22044  lsslindf  22046  lsslinds  22047  issubassa  22085  sraassab  22086  issubassa2  22110  gsumbagdiag  22150  subrgasclcl  22286  ply1scleq  22533  matunit  22903  slesolinvbi  22909  en2top  23213  elcls  23301  neindisj2  23351  neiptopnei  23360  neiptopreu  23361  maxlp  23375  neitr  23408  iscncl  23497  cncnp  23508  isreg2  23605  dis2ndc  23689  1stccnp  23691  islly2  23713  dislly  23726  dissnlocfin  23758  kgencmp2  23775  pt1hmeo  24035  xkocnv  24043  t0kq  24047  uffixfr  24152  flimcf  24211  cnpflf2  24229  fclscf  24254  cnextf  24295  utopsnneiplem  24476  isucn2  24507  cfilucfil  24788  psmetutop  24796  restmetu  24799  tngngp2  24881  tngngp  24883  nmoleub  24960  metdseq0  25084  cnheibor  25186  pcophtb  25260  nmoleub2lem  25345  lmmbr  25489  iscfil3  25504  cmetss  25547  cldcss  25672  mbfeqalem2  25873  mbfposb  25884  itg2const2  25972  itgss3  26045  plyco0  26420  dgrlt  26495  ulm2  26624  coseq00topi  26743  coseq0negpitopi  26744  sineq0  26764  relogbcxpb  27027  atans2  27171  xrlimcnp  27208  dchrelbas2  27476  dchrn0  27489  2sqb  27671  nosupbnd2  27955  noinfbnd2  27970  lesrec  28067  ltmuls2  28439  elreno2  28763  istrkg2ld  28804  tgcgreqb  28825  tgbtwncomb  28834  trgcgrg  28860  legov  28930  legov2  28931  legov3  28943  hlbtwn  28959  tglineelsb2  28982  tglinecom  28985  colline  29000  mirinv  29020  mirbtwnb  29026  mirbtwnhl  29034  mirleqb  29048  perpcom  29070  isperp2  29072  oppcom  29102  opphllem3  29107  lnopp2hpgb  29123  colopp  29129  colhp  29130  plngcplem  29145  plngrotlem2  29148  lmieu  29171  iscgra1  29199  dfcgra2  29220  ragsupplcgra  29227  cgraer  29259  angmgmaddeu1  29261  angmgmaddeu2  29262  angmgmaddeu3  29263  angmgmaddeu4  29264  angmgmaddeu5  29265  angmgmaddeu6  29266  angmgmaddeu7  29267  angmgmaddov2lem  29269  angmgmaddcpbl  29272  dfprlng2  29307  edgnbusgreu  29830  nb3grprlem1  29843  lfgriswlk  30153  eleclclwwlknlem2  30534  clwwlknscsh  30535  clwwlknon1  30570  numclwwlk2lem1  30859  grpoinvid1  31012  grpoinvid2  31013  leopmul  32618  hst1h  32711  eqelbid  32953  diffib  32999  ifnebib  33027  iinabrex  33045  disjabrex  33058  disjabrexf  33059  erbr3b  33093  f1o3d  33102  funimass4f  33113  2ndimaxp  33122  fgreu  33147  fcnvgreu  33148  1stpreimas  33181  fcobij  33194  cocnvf1o  33203  resf1o  33204  nn0xmulclb  33245  fzsplit3  33267  fzo0opth  33277  sgnmulsgp  33305  eliccioo  33379  mgcmntco  33437  dfmgc2lem  33438  dfmgc2  33439  pwrssmgc  33443  mgcf1o  33446  mndlrinvb  33468  mndlactfo  33470  mndractfo  33472  mndlactf1o  33473  mndractf1o  33474  gsumhashmul  33510  gsumwrd2dccatlem  33520  cyc3genpm  33595  isarchi3  33630  prmsimpcyc  33671  elrgspnsubrunlem1  33690  elrgspnsubrun  33692  rlocisunit  33719  ricdomn  33733  fracerl  33750  dvdsruasso  33821  dvdsruasso2  33822  dvdsrspss  33823  grplsmid  33836  quslsm  33837  nsgmgc  33844  nsgqusf1olem2  33846  nsgqusf1olem3  33847  pidlnzb  33853  unitpidl1  33855  elrspunidl  33859  elrspunsn  33860  drngidlhash  33864  mxidlirred  33878  mxidlnzrb  33885  qsdrng  33902  dflring3  33910  dflring4  33911  rsprprmprmidlb  33936  rprmirredb  33945  deg1le0eq0  33986  ply1unit  33988  0mplrim  34027  selvply1rhmlem2  34034  evlextv  34055  mplvrpmrhm  34060  esplyfv1  34082  esplyfval1  34086  esplyfvaln  34087  esplyind  34088  lvecdim0  34120  extdg1b  34180  fldextrspunlsp  34187  irngnzply1  34204  1smat1  34317  ist0cld  34346  qtophaus  34349  reff  34352  locfinreflem  34353  cmpcref  34363  zarcls1  34382  zarclsun  34383  zarclsiin  34384  zarclssn  34386  metider  34407  pstmfval  34409  qqhval2  34495  aean  34758  imambfm  34776  eulerpartlemgvv  34890  orvcgteel  34982  orvclteel  34987  ballotlemsf1o  35028  actfunsnf1o  35115  reprsuc  35126  reprpmtf1o  35137  sconnpi1  35821  brofs2  36660  brifs2  36661  broutsideof2  36705  ttc0elw  37149  bj-abv  37652  irrdiff  38081  ltflcei  38365  poimirlem25  38397  ismblfin  38413  cnambfre  38420  ftc1anclem6  38450  ismndo1  38626  isdrngo2  38711  eqvrelsymb  39441  eqvrelth  39446  lshpnelb  39860  lshpnel2N  39861  lsatspn0  39876  lsatelbN  39882  lsat0cv  39909  lcvexch  39915  lcv1  39917  lkrshp3  39982  lkrpssN  40039  lkrss2N  40045  cvlsupr2  40219  atcvrlln  40396  llncvrlpln  40434  2llnmj  40436  lplncvrlvol  40492  2lplnmj  40498  polcon2bN  40796  pcl0bN  40799  lhpmcvr3  40901  lhpmatb  40907  ltrncoidN  41004  ltrneq3  41084  ltrniotavalbN  41460  cdlemg1cN  41463  diclspsn  42070  dihopelvalcpre  42124  dihord4  42134  dihord  42140  dihmeetlem4preN  42182  dih1dimatlem0  42204  dochsscl  42244  dochoccl  42245  dochord  42246  dochsat  42259  dochshpncl  42260  dochsatshpb  42328  dochshpsat  42330  mapdval4N  42508  mapdsn  42517  hdmap14lem12  42755  hdmapip0  42791  hlhillcs  42834  resuppsinopn  43241  mulgt0b2d  43369  mullt0b1d  43374  mullt0b2d  43375  riccrng  43407  ricdrng  43414  prjspner1  43475  mrefg2  43555  mzpmfp  43595  lzenom  43618  elpell14qr2  43706  elpell1qr2  43716  pellfund14b  43743  congabseq  43818  acongeq  43827  jm2.23  43840  jm2.20nn  43841  jm2.25lem1  43842  wepwsolem  43886  islssfg2  43915  lnmlmic  43932  dfacbasgrp  43952  unielss  44062  rfovcnvf1od  44847  dssmapnvod  44863  ntrclscls00  44909  rfcnpre3  45870  rfcnpre4  45871  ssmapsn  46049  rnmptssbi  46092  infxrgelbrnmpt  46285  xnegre  46297  xrpnf  46316  rexanuz2nf  46323  ioossioobi  46350  iccshift  46351  iocopn  46353  eliccelioc  46354  iooshift  46355  icoopn  46358  qinioo  46368  limcdm0  46451  islptre  46452  islpcn  46470  limcresioolb  46474  climuzlem  46574  climlimsup  46591  liminfgelimsup  46613  liminfgelimsupuz  46619  climliminf  46637  climliminflimsup  46639  climliminflimsup2  46640  xlimpnfxnegmnf  46645  xlimbr  46658  xlimmnfv  46665  xlimpnfv  46669  xlimclim2  46671  dfxlim2v  46678  climresdm  46681  xlimresdm  46690  xlimliminflimsup  46693  fperdvper  46750  itgperiod  46812  fourierdlem32  46970  fourierdlem33  46971  fourierdlem48  46985  fourierdlem49  46986  fourierdlem71  47008  fourierdlem81  47018  preimagelt  47530  preimalegt  47531  smfliminflem  47661  smfliminfmpt  47663  chnsubseqwl  47710  fcoresfob  47963  m1mod0mod1  48251  uhgrimedg  48810  isubgr3stgrlem8  48892  rngcinvALTV  49194  ringcinvALTV  49228  xpco2  49788  fvconstr  49793  fvconstrn0  49794  lubeldm2  49885  glbeldm2  49886  upeu2lem  49957  sectpropd  49966  invpropd  49968  isopropd  49970  cicerALT  49975  cicpropd  49979  up1st2ndb  50116  uobffth  50147  uobeqw  50148  natoppfb  50160  oppc1stflem  50216  fucofulem1  50239  functhinclem1  50373  fullthinc  50379  thincciso4  50386  thinciso  50399  functermclem  50436  termcterm3  50444  termcciso  50445  termcarweu  50457  termfucterm  50473  prstchom2ALT  50493  lanval2  50556  ranval2  50559