Theorem impbida 812

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 417	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		impbida.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
4	3	ex 417	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 215	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biadanid  834  bibiad  852  frsn  5749  funfvbrb  7046  iinpreima  7064  fcdmssb  7117  fnprb  7206  fntpb  7207  fpr2g  7209  nvocnv  7279  fsnex  7281  f1ocnv2d  7663  resf1extb  7927  el2xptp0  8029  1stconst  8091  2ndconst  8092  cnvf1o  8102  fimaproj  8127  tfrlem15  8375  oeeui  8584  ersymb  8705  swoer  8722  erth  8745  boxriin  8934  boxcutc  8935  domunsncan  9061  pw2f1olem  9065  enen1  9101  enen2  9102  domen1  9103  domen2  9104  sdomen1  9105  sdomen2  9106  xpmapenlem  9128  ensymfib  9164  ordiso2  9473  wdomen1  9534  wdomen2  9535  fin23lem26  10304  fpwwe2lem7  10617  r1wunlim  10717  mul2lt0bi  13119  ixxun  13383  xov1plusxeqvd  13520  fzsplit2  13573  fseq1p1m1  13622  elfz2nn0  13642  flflp1  13836  modaddb  13938  modsubdir  13972  zesq  14258  expnngt1b  14274  hashprg  14427  hashgt0elexb  14434  hashbclem  14485  hashge2el2difb  14515  sgn3da  15134  sgnnbi  15137  sgnpbi  15138  sgnmulsgn  15142  rereb  15167  rlimclim  15593  iserex  15704  caucvgb  15727  mptfzshft  15825  fsumrev  15826  climcnds  15901  fprodrev  16027  dvdsadd2b  16359  nn0ob  16437  bitsfzo  16488  dfgcd2  16599  dvdsmulgcd  16609  lcmgcdeq  16665  qden1elz  16811  mrcidb  17666  mrieqvlemd  17680  isacs2  17704  cicer  17858  ssclem  17871  issubc3  17901  ffthiso  17983  fuciso  18030  setcmon  18139  setcepi  18140  setcinv  18142  catciso  18163  acsfiindd  18604  issstrmgm  18706  mgmhmf1o  18753  issubmgm2  18756  subsubmgm  18763  resmgmhm2b  18766  issubmnd  18814  mhmf1o  18849  subsubm  18870  resmhm2b  18876  grpinvid1  19053  grpinvid2  19054  subsubg  19211  ssnmz  19227  qsxpid  19238  ghmf1  19311  kerf1ghm  19312  ghmf1o  19313  conjnmzb  19318  subggim  19331  gicsubgen  19344  ghmqusnsglem1  19345  ghmquskerlem1  19348  ghmqusker  19352  gass  19366  odf1  19627  gex1  19656  fislw  19690  sylow3lem2  19693  sylow3lem6  19697  lsmdisj2a  19752  lsmdisj2b  19753  efgred2  19818  dmdprdsplit  20114  2nsgsimpgd  20169  simpgnsgbid  20170  ablsimpgd  20183  ogrpinv0le  20201  ogrpaddltbi  20204  ogrpaddltrbid  20206  ogrpinv0lt  20208  0unit  20474  irrednegb  20509  rnghmf1o  20530  rhmf1o  20575  subsubrng  20662  subrgunit  20689  subsubrg  20697  rngcinv  20736  ringcinv  20770  isdrng4  20839  isdrng2  20843  isdrng3  20853  issubdrg  20883  islss3  21080  islss4  21083  ellspsn6  21115  lspsneq0b  21134  islmhm2  21159  lmhmf1o  21167  reslmhm2b  21175  lssvs0or  21234  lvecinv  21237  ellspsn4  21248  lspdisjb  21250  islbs2  21278  islbs3  21279  dflidl2rng  21343  drngidl  21385  rngringbd  21448  isprmidlc  21472  prmidl0  21478  qsidom  21482  prmirredlem  21622  islindf3  21976  lindsmm  21978  lsslindf  21980  lsslinds  21981  issubassa  22017  sraassab  22018  issubassa2  22042  gsumbagdiag  22082  subrgasclcl  22218  ply1scleq  22465  matunit  22835  slesolinvbi  22838  en2top  23142  elcls  23230  neindisj2  23280  neiptopnei  23289  neiptopreu  23290  maxlp  23304  neitr  23337  iscncl  23426  cncnp  23437  isreg2  23534  dis2ndc  23617  1stccnp  23619  islly2  23641  dislly  23654  dissnlocfin  23686  kgencmp2  23703  pt1hmeo  23963  xkocnv  23971  t0kq  23975  uffixfr  24080  flimcf  24139  cnpflf2  24157  fclscf  24182  cnextf  24223  utopsnneiplem  24404  isucn2  24435  cfilucfil  24716  psmetutop  24724  restmetu  24727  tngngp2  24809  tngngp  24811  nmoleub  24888  metdseq0  25012  cnheibor  25114  pcophtb  25188  nmoleub2lem  25273  lmmbr  25417  iscfil3  25432  cmetss  25475  cldcss  25600  mbfeqalem2  25801  mbfposb  25812  itg2const2  25900  itgss3  25974  plyco0  26349  dgrlt  26423  ulm2  26548  coseq00topi  26667  coseq0negpitopi  26668  sineq0  26689  relogbcxpb  26952  atans2  27096  xrlimcnp  27133  dchrelbas2  27401  dchrn0  27414  2sqb  27596  nosupbnd2  27880  noinfbnd2  27895  lesrec  27992  ltmuls2  28364  elreno2  28688  istrkg2ld  28729  tgcgreqb  28750  tgbtwncomb  28758  trgcgrg  28784  legov  28854  legov2  28855  legov3  28867  hlbtwn  28883  tglineelsb2  28905  tglinecom  28908  colline  28923  mirinv  28943  mirbtwnb  28949  mirbtwnhl  28957  mirleqb  28971  perpcom  28993  isperp2  28995  oppcom  29025  opphllem3  29030  lnopp2hpgb  29045  colopp  29051  colhp  29052  plngcplem  29067  plngrotlem2  29070  lmieu  29093  iscgra1  29121  dfcgra2  29141  ragsupplcgra  29148  dfprlng2  29197  edgnbusgreu  29717  nb3grprlem1  29730  lfgriswlk  30036  eleclclwwlknlem2  30412  clwwlknscsh  30413  clwwlknon1  30448  numclwwlk2lem1  30727  grpoinvid1  30880  grpoinvid2  30881  leopmul  32486  hst1h  32579  eqelbid  32821  diffib  32867  ifnebib  32895  iinabrex  32914  disjabrex  32927  disjabrexf  32928  erbr3b  32962  f1o3d  32971  funimass4f  32982  2ndimaxp  32991  fgreu  33016  fcnvgreu  33017  1stpreimas  33051  fcobij  33065  cocnvf1o  33074  resf1o  33075  nn0xmulclb  33116  fzsplit3  33138  fzo0opth  33148  sgnmulsgp  33176  eliccioo  33250  mgcmntco  33314  dfmgc2lem  33315  dfmgc2  33316  pwrssmgc  33320  mgcf1o  33323  mndlrinvb  33345  mndlactfo  33347  mndractfo  33349  mndlactf1o  33350  mndractf1o  33351  gsumhashmul  33387  gsumwrd2dccatlem  33397  cyc3genpm  33472  isarchi3  33507  prmsimpcyc  33548  elrgspnsubrunlem1  33567  elrgspnsubrun  33569  rlocisunit  33596  ricdomn  33610  fracerl  33627  dvdsruasso  33698  dvdsruasso2  33699  dvdsrspss  33700  grplsmid  33713  quslsm  33714  nsgmgc  33721  nsgqusf1olem2  33723  nsgqusf1olem3  33724  pidlnzb  33730  unitpidl1  33732  elrspunidl  33736  elrspunsn  33737  drngidlhash  33741  mxidlirred  33755  mxidlnzrb  33762  qsdrng  33779  dflring3  33787  dflring4  33788  rsprprmprmidlb  33813  rprmirredb  33822  deg1le0eq0  33863  ply1unit  33865  0mplrim  33904  selvply1rhmlem2  33911  evlextv  33932  mplvrpmrhm  33937  esplyfv1  33959  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  lvecdim0  33997  extdg1b  34057  fldextrspunlsp  34064  irngnzply1  34081  1smat1  34194  ist0cld  34223  qtophaus  34226  reff  34229  locfinreflem  34230  cmpcref  34240  zarcls1  34259  zarclsun  34260  zarclsiin  34261  zarclssn  34263  metider  34284  pstmfval  34286  qqhval2  34372  aean  34634  imambfm  34652  eulerpartlemgvv  34766  orvcgteel  34858  orvclteel  34863  ballotlemsf1o  34904  actfunsnf1o  34991  reprsuc  35002  reprpmtf1o  35013  sconnpi1  35731  brofs2  36569  brifs2  36570  broutsideof2  36614  ttc0elw  37058  bj-abv  37561  irrdiff  37990  ltflcei  38279  poimirlem25  38316  ismblfin  38332  cnambfre  38339  ftc1anclem6  38369  ismndo1  38544  isdrngo2  38629  eqvrelsymb  39359  eqvrelth  39364  lshpnelb  39778  lshpnel2N  39779  lsatspn0  39794  lsatelbN  39800  lsat0cv  39827  lcvexch  39833  lcv1  39835  lkrshp3  39900  lkrpssN  39957  lkrss2N  39963  cvlsupr2  40137  atcvrlln  40314  llncvrlpln  40352  2llnmj  40354  lplncvrlvol  40410  2lplnmj  40416  polcon2bN  40714  pcl0bN  40717  lhpmcvr3  40819  lhpmatb  40825  ltrncoidN  40922  ltrneq3  41002  ltrniotavalbN  41378  cdlemg1cN  41381  diclspsn  41988  dihopelvalcpre  42042  dihord4  42052  dihord  42058  dihmeetlem4preN  42100  dih1dimatlem0  42122  dochsscl  42162  dochoccl  42163  dochord  42164  dochsat  42177  dochshpncl  42178  dochsatshpb  42246  dochshpsat  42248  mapdval4N  42426  mapdsn  42435  hdmap14lem12  42673  hdmapip0  42709  hlhillcs  42752  resuppsinopn  43144  mulgt0b2d  43272  mullt0b1d  43277  mullt0b2d  43278  riccrng  43310  ricdrng  43317  prjspner1  43378  mrefg2  43458  mzpmfp  43498  lzenom  43521  elpell14qr2  43609  elpell1qr2  43619  pellfund14b  43646  congabseq  43721  acongeq  43730  jm2.23  43743  jm2.20nn  43744  jm2.25lem1  43745  wepwsolem  43789  islssfg2  43818  lnmlmic  43835  dfacbasgrp  43855  unielss  43965  rfovcnvf1od  44750  dssmapnvod  44766  ntrclscls00  44812  rfcnpre3  45773  rfcnpre4  45774  ssmapsn  45952  rnmptssbi  45995  infxrgelbrnmpt  46188  xnegre  46200  xrpnf  46219  rexanuz2nf  46226  ioossioobi  46253  iccshift  46254  iocopn  46256  eliccelioc  46257  iooshift  46258  icoopn  46261  qinioo  46271  limcdm0  46354  islptre  46355  islpcn  46373  limcresioolb  46377  climuzlem  46477  climlimsup  46494  liminfgelimsup  46516  liminfgelimsupuz  46522  climliminf  46540  climliminflimsup  46542  climliminflimsup2  46543  xlimpnfxnegmnf  46548  xlimbr  46561  xlimmnfv  46568  xlimpnfv  46572  xlimclim2  46574  dfxlim2v  46581  climresdm  46584  xlimresdm  46593  xlimliminflimsup  46596  fperdvper  46653  itgperiod  46715  fourierdlem32  46873  fourierdlem33  46874  fourierdlem48  46888  fourierdlem49  46889  fourierdlem71  46911  fourierdlem81  46921  preimagelt  47433  preimalegt  47434  smfliminflem  47564  smfliminfmpt  47566  chnsubseqwl  47615  fcoresfob  47829  m1mod0mod1  48117  uhgrimedg  48676  isubgr3stgrlem8  48758  rngcinvALTV  49061  ringcinvALTV  49095  xpco2  49655  fvconstr  49660  fvconstrn0  49661  lubeldm2  49754  glbeldm2  49755  upeu2lem  49826  sectpropd  49835  invpropd  49837  isopropd  49839  cicerALT  49844  cicpropd  49848  up1st2ndb  49985  uobffth  50016  uobeqw  50017  natoppfb  50029  oppc1stflem  50085  fucofulem1  50108  functhinclem1  50242  fullthinc  50248  thincciso4  50255  thinciso  50268  functermclem  50305  termcterm3  50313  termcciso  50314  termcarweu  50326  termfucterm  50342  prstchom2ALT  50362  lanval2  50425  ranval2  50428