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  5751  funfvbrb  7050  iinpreima  7068  fcdmssb  7121  fnprb  7213  fntpb  7214  fpr2g  7216  nvocnv  7288  fsnex  7290  f1ocnv2d  7673  resf1extb  7937  el2xptp0  8039  1stconst  8101  2ndconst  8102  cnvf1o  8112  fimaproj  8137  tfrlem15  8385  oeeui  8594  ersymb  8715  swoer  8732  erth  8755  boxriin  8944  boxcutc  8945  domunsncan  9072  pw2f1olem  9076  enen1  9112  enen2  9113  domen1  9114  domen2  9115  sdomen1  9116  sdomen2  9117  xpmapenlem  9139  ensymfib  9175  ordiso2  9484  wdomen1  9545  wdomen2  9546  fin23lem26  10324  fpwwe2lem7  10639  r1wunlim  10739  mul2lt0bi  13142  ixxun  13406  xov1plusxeqvd  13543  fzsplit2  13596  fseq1p1m1  13645  elfz2nn0  13665  flflp1  13860  modaddb  13962  modsubdir  13996  zesq  14282  expnngt1b  14298  hashprg  14451  hashgt0elexb  14458  hashbclem  14509  hashge2el2difb  14539  sgn3da  15164  sgnnbi  15167  sgnpbi  15168  sgnmulsgn  15172  rereb  15197  rlimclim  15623  iserex  15734  caucvgb  15757  mptfzshft  15854  fsumrev  15855  climcnds  15930  fprodrev  16056  dvdsadd2b  16388  nn0ob  16466  bitsfzo  16517  dfgcd2  16628  dvdsmulgcd  16638  lcmgcdeq  16694  qden1elz  16840  mrcidb  17695  mrieqvlemd  17709  isacs2  17733  cicer  17887  ssclem  17900  issubc3  17930  ffthiso  18012  fuciso  18059  setcmon  18168  setcepi  18169  setcinv  18171  catciso  18192  acsfiindd  18633  issstrmgm  18737  mgmhmf1o  18792  issubmgm2  18795  subsubmgm  18802  resmgmhm2b  18805  issubmnd  18856  mhmf1o  18893  subsubm  18914  resmhm2b  18920  grpinvid1  19104  grpinvid2  19105  subsubg  19262  ssnmz  19278  qsxpid  19289  ghmf1  19362  kerf1ghm  19363  ghmf1o  19364  conjnmzb  19369  subggim  19382  gicsubgen  19395  ghmqusnsglem1  19396  ghmquskerlem1  19399  ghmqusker  19403  gass  19417  odf1  19678  gex1  19707  fislw  19741  sylow3lem2  19744  sylow3lem6  19748  lsmdisj2a  19803  lsmdisj2b  19804  efgred2  19869  dmdprdsplit  20165  2nsgsimpgd  20220  simpgnsgbid  20221  ablsimpgd  20234  ogrpinv0le  20252  ogrpaddltbi  20255  ogrpaddltrbid  20257  ogrpinv0lt  20259  0unit  20526  irrednegb  20561  rnghmf1o  20582  rhmf1o  20627  subsubrng  20714  subrgunit  20741  subsubrg  20749  rngcinv  20788  ringcinv  20822  isdrng4  20891  isdrng2  20895  isdrng3  20905  issubdrg  20935  islss3  21132  islss4  21135  ellspsn6  21167  lspsneq0b  21186  islmhm2  21211  lmhmf1o  21219  reslmhm2b  21227  lssvs0or  21286  lvecinv  21289  ellspsn4  21300  lspdisjb  21302  islbs2  21330  islbs3  21331  dflidl2rng  21395  drngidl  21437  rngringbd  21500  isprmidlc  21524  prmidl0  21530  qsidom  21534  prmirredlem  21674  islindf3  22028  lindsmm  22030  lsslindf  22032  lsslinds  22033  issubassa  22069  sraassab  22070  issubassa2  22094  gsumbagdiag  22134  subrgasclcl  22270  ply1scleq  22517  matunit  22887  slesolinvbi  22890  en2top  23194  elcls  23282  neindisj2  23332  neiptopnei  23341  neiptopreu  23342  maxlp  23356  neitr  23389  iscncl  23478  cncnp  23489  isreg2  23586  dis2ndc  23670  1stccnp  23672  islly2  23694  dislly  23707  dissnlocfin  23739  kgencmp2  23756  pt1hmeo  24016  xkocnv  24024  t0kq  24028  uffixfr  24133  flimcf  24192  cnpflf2  24210  fclscf  24235  cnextf  24276  utopsnneiplem  24457  isucn2  24488  cfilucfil  24769  psmetutop  24777  restmetu  24780  tngngp2  24862  tngngp  24864  nmoleub  24941  metdseq0  25065  cnheibor  25167  pcophtb  25241  nmoleub2lem  25326  lmmbr  25470  iscfil3  25485  cmetss  25528  cldcss  25653  mbfeqalem2  25854  mbfposb  25865  itg2const2  25953  itgss3  26027  plyco0  26402  dgrlt  26476  ulm2  26601  coseq00topi  26720  coseq0negpitopi  26721  sineq0  26742  relogbcxpb  27005  atans2  27149  xrlimcnp  27186  dchrelbas2  27454  dchrn0  27467  2sqb  27649  nosupbnd2  27933  noinfbnd2  27948  lesrec  28045  ltmuls2  28417  elreno2  28741  istrkg2ld  28782  tgcgreqb  28803  tgbtwncomb  28811  trgcgrg  28837  legov  28907  legov2  28908  legov3  28920  hlbtwn  28936  tglineelsb2  28958  tglinecom  28961  colline  28976  mirinv  28996  mirbtwnb  29002  mirbtwnhl  29010  mirleqb  29024  perpcom  29046  isperp2  29048  oppcom  29078  opphllem3  29083  lnopp2hpgb  29098  colopp  29104  colhp  29105  plngcplem  29120  plngrotlem2  29123  lmieu  29146  iscgra1  29174  dfcgra2  29194  ragsupplcgra  29201  dfprlng2  29254  edgnbusgreu  29777  nb3grprlem1  29790  lfgriswlk  30100  eleclclwwlknlem2  30481  clwwlknscsh  30482  clwwlknon1  30517  numclwwlk2lem1  30800  grpoinvid1  30953  grpoinvid2  30954  leopmul  32559  hst1h  32652  eqelbid  32894  diffib  32940  ifnebib  32968  iinabrex  32987  disjabrex  33000  disjabrexf  33001  erbr3b  33035  f1o3d  33044  funimass4f  33055  2ndimaxp  33064  fgreu  33089  fcnvgreu  33090  1stpreimas  33124  fcobij  33137  cocnvf1o  33146  resf1o  33147  nn0xmulclb  33188  fzsplit3  33210  fzo0opth  33220  sgnmulsgp  33248  eliccioo  33322  mgcmntco  33380  dfmgc2lem  33381  dfmgc2  33382  pwrssmgc  33386  mgcf1o  33389  mndlrinvb  33411  mndlactfo  33413  mndractfo  33415  mndlactf1o  33416  mndractf1o  33417  gsumhashmul  33453  gsumwrd2dccatlem  33463  cyc3genpm  33538  isarchi3  33573  prmsimpcyc  33614  elrgspnsubrunlem1  33633  elrgspnsubrun  33635  rlocisunit  33662  ricdomn  33676  fracerl  33693  dvdsruasso  33764  dvdsruasso2  33765  dvdsrspss  33766  grplsmid  33779  quslsm  33780  nsgmgc  33787  nsgqusf1olem2  33789  nsgqusf1olem3  33790  pidlnzb  33796  unitpidl1  33798  elrspunidl  33802  elrspunsn  33803  drngidlhash  33807  mxidlirred  33821  mxidlnzrb  33828  qsdrng  33845  dflring3  33853  dflring4  33854  rsprprmprmidlb  33879  rprmirredb  33888  deg1le0eq0  33929  ply1unit  33931  0mplrim  33970  selvply1rhmlem2  33977  evlextv  33998  mplvrpmrhm  34003  esplyfv1  34025  esplyfval1  34029  esplyfvaln  34030  esplyind  34031  lvecdim0  34063  extdg1b  34123  fldextrspunlsp  34130  irngnzply1  34147  1smat1  34260  ist0cld  34289  qtophaus  34292  reff  34295  locfinreflem  34296  cmpcref  34306  zarcls1  34325  zarclsun  34326  zarclsiin  34327  zarclssn  34329  metider  34350  pstmfval  34352  qqhval2  34438  aean  34701  imambfm  34719  eulerpartlemgvv  34833  orvcgteel  34925  orvclteel  34930  ballotlemsf1o  34971  actfunsnf1o  35058  reprsuc  35069  reprpmtf1o  35080  sconnpi1  35770  brofs2  36608  brifs2  36609  broutsideof2  36653  ttc0elw  37097  bj-abv  37600  irrdiff  38029  ltflcei  38318  poimirlem25  38355  ismblfin  38371  cnambfre  38378  ftc1anclem6  38408  ismndo1  38584  isdrngo2  38669  eqvrelsymb  39399  eqvrelth  39404  lshpnelb  39818  lshpnel2N  39819  lsatspn0  39834  lsatelbN  39840  lsat0cv  39867  lcvexch  39873  lcv1  39875  lkrshp3  39940  lkrpssN  39997  lkrss2N  40003  cvlsupr2  40177  atcvrlln  40354  llncvrlpln  40392  2llnmj  40394  lplncvrlvol  40450  2lplnmj  40456  polcon2bN  40754  pcl0bN  40757  lhpmcvr3  40859  lhpmatb  40865  ltrncoidN  40962  ltrneq3  41042  ltrniotavalbN  41418  cdlemg1cN  41421  diclspsn  42028  dihopelvalcpre  42082  dihord4  42092  dihord  42098  dihmeetlem4preN  42140  dih1dimatlem0  42162  dochsscl  42202  dochoccl  42203  dochord  42204  dochsat  42217  dochshpncl  42218  dochsatshpb  42286  dochshpsat  42288  mapdval4N  42466  mapdsn  42475  hdmap14lem12  42713  hdmapip0  42749  hlhillcs  42792  resuppsinopn  43184  mulgt0b2d  43312  mullt0b1d  43317  mullt0b2d  43318  riccrng  43350  ricdrng  43357  prjspner1  43418  mrefg2  43498  mzpmfp  43538  lzenom  43561  elpell14qr2  43649  elpell1qr2  43659  pellfund14b  43686  congabseq  43761  acongeq  43770  jm2.23  43783  jm2.20nn  43784  jm2.25lem1  43785  wepwsolem  43829  islssfg2  43858  lnmlmic  43875  dfacbasgrp  43895  unielss  44005  rfovcnvf1od  44790  dssmapnvod  44806  ntrclscls00  44852  rfcnpre3  45813  rfcnpre4  45814  ssmapsn  45992  rnmptssbi  46035  infxrgelbrnmpt  46228  xnegre  46240  xrpnf  46259  rexanuz2nf  46266  ioossioobi  46293  iccshift  46294  iocopn  46296  eliccelioc  46297  iooshift  46298  icoopn  46301  qinioo  46311  limcdm0  46394  islptre  46395  islpcn  46413  limcresioolb  46417  climuzlem  46517  climlimsup  46534  liminfgelimsup  46556  liminfgelimsupuz  46562  climliminf  46580  climliminflimsup  46582  climliminflimsup2  46583  xlimpnfxnegmnf  46588  xlimbr  46601  xlimmnfv  46608  xlimpnfv  46612  xlimclim2  46614  dfxlim2v  46621  climresdm  46624  xlimresdm  46633  xlimliminflimsup  46636  fperdvper  46693  itgperiod  46755  fourierdlem32  46913  fourierdlem33  46914  fourierdlem48  46928  fourierdlem49  46929  fourierdlem71  46951  fourierdlem81  46961  preimagelt  47473  preimalegt  47474  smfliminflem  47604  smfliminfmpt  47606  chnsubseqwl  47655  fcoresfob  47869  m1mod0mod1  48157  uhgrimedg  48716  isubgr3stgrlem8  48798  rngcinvALTV  49100  ringcinvALTV  49134  xpco2  49694  fvconstr  49699  fvconstrn0  49700  lubeldm2  49793  glbeldm2  49794  upeu2lem  49865  sectpropd  49874  invpropd  49876  isopropd  49878  cicerALT  49883  cicpropd  49887  up1st2ndb  50024  uobffth  50055  uobeqw  50056  natoppfb  50068  oppc1stflem  50124  fucofulem1  50147  functhinclem1  50281  fullthinc  50287  thincciso4  50294  thinciso  50307  functermclem  50344  termcterm3  50352  termcciso  50353  termcarweu  50365  termfucterm  50381  prstchom2ALT  50401  lanval2  50464  ranval2  50467