MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi1d Structured version   Visualization version   GIF version

Theorem imbi1d 331
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimprd 238 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 82 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 219 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 82 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 202 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  imbi12d  334  imbi1  337  imim21b  382  pm5.33  921  con3ALT  1031  con3OLD  1034  19.21t  2071  19.21tOLDOLD  2072  19.21tOLD  2212  axc15  2302  ax12v2OLD  2341  drsb1  2376  ralcom2  3098  raleqf  3127  ralxpxfr2d  3316  alexeqg  3320  mo2icl  3372  sbc19.21g  3489  csbiebg  3542  ralss  3653  r19.37zv  4045  ssuniOLD  4433  intmin4  4478  ssexg  4774  pocl  5012  vtoclr  5134  frsn  5160  fun11  5931  funimass4  6214  dff13  6477  f1mpt  6483  isopolem  6560  oprabid  6642  caovcan  6803  caoftrn  6897  ordunisuc2  7006  tfisi  7020  tfinds  7021  tfindsg  7022  tfindsg2  7023  dfom2  7029  findsg  7055  frxp  7247  dfsmo2  7404  qliftfun  7792  ecoptocl  7797  ecopovtrn  7810  dom2lem  7955  findcard  8159  findcard2  8160  findcard3  8163  fiint  8197  supmo  8318  eqsup  8322  suplub  8326  supisoex  8340  infmo  8361  wemaplem1  8411  wemaplem2  8412  wemapsolem  8415  oemapvali  8541  cantnf  8550  wemapwe  8554  karden  8718  aceq1  8900  zorn2lem1  9278  axrepndlem2  9375  axregndlem2  9385  pwfseqlem4  9444  gruurn  9580  indpi  9689  nqereu  9711  prcdnq  9775  supexpr  9836  ltsosr  9875  supsrlem  9892  supsr  9893  axpre-lttrn  9947  axpre-sup  9950  prodgt0  10828  infm3  10942  prime  11418  raluz  11696  zsupss  11737  uzsupss  11740  xrsupsslem  12096  xrinfmsslem  12097  fz1sbc  12373  ssnn0fi  12740  fi1uzind  13234  brfi1indALT  13237  fi1uzindOLD  13240  brfi1indALTOLD  13243  wrdind  13430  wrd2ind  13431  relexprelg  13728  rtrclreclem3  13750  relexpindlem  13753  relexpind  13754  rtrclind  13755  rexanre  14036  rexico  14043  limsupgle  14158  rlim2lt  14178  rlim3  14179  ello12  14197  ello12r  14198  ello1d  14204  elo12  14208  elo12r  14209  rlimconst  14225  lo1resb  14245  o1resb  14247  rlimcn2  14271  addcn2  14274  mulcn2  14276  reccn2  14277  cn1lem  14278  o1rlimmul  14299  lo1le  14332  caucvgrlem  14353  divrcnv  14528  rpnnen2lem12  14898  sqrt2irr  14922  dfgcd2  15206  exprmfct  15359  isprm5  15362  isprm7  15363  prmdvdsexpr  15372  prmpwdvds  15551  vdwmc2  15626  ramtlecl  15647  ramub  15660  rami  15662  ramcl  15676  firest  16033  mreexexd  16248  mreexexdOLD  16249  acsfn  16260  prslem  16871  ispos  16887  posi  16890  isposd  16895  lubeldm  16921  lubval  16924  glbeldm  16934  glbval  16937  joinval2lem  16948  meetval2lem  16962  pospropd  17074  odlem1  17894  mndodcongi  17902  gexlem1  17934  sylow1lem3  17955  efgredlemb  18099  efgred  18101  frgpnabllem1  18216  isrrg  19228  mplsubglem  19374  mpllsslem  19375  ltbval  19411  opsrval  19414  xrsdsreclb  19733  islindf4  20117  mdetunilem1  20358  mdetunilem3  20360  mdetunilem4  20361  mdetunilem9  20366  chpscmat  20587  chfacffsupp  20601  chfacfscmulfsupp  20604  chfacfpmmulfsupp  20608  istopg  20640  isclo2  20832  neiptoptop  20875  neiptopnei  20876  lmbr  21002  ist0  21064  ist1-2  21091  t1sep2  21113  cmpfi  21151  2ndcdisj  21199  1stccn  21206  iskgen3  21292  ptpjopn  21355  hausdiag  21388  xkopt  21398  ist0-4  21472  isr0  21480  r0sep  21491  fbfinnfr  21585  fmfnfmlem2  21699  fmfnfmlem4  21701  fmfnfm  21702  cnflf  21746  cnfcf  21786  tmdgsum2  21840  tsmsgsum  21882  tsmsres  21887  tsmsf1o  21888  tsmsxplem1  21896  tsmsxp  21898  ustssel  21949  ustincl  21951  ustdiag  21952  ustinvel  21953  ustexhalf  21954  ust0  21963  ustuqtop4  21988  utopsnneiplem  21991  isucn2  22023  iducn  22027  metcnp  22286  metcnpi3  22291  txmetcnp  22292  metucn  22316  ngptgp  22380  nlmvscnlem1  22430  nrginvrcnlem  22435  nghmcn  22489  xrge0tsms  22577  xmetdcn2  22580  metdscn  22599  addcnlem  22607  elcncf1di  22638  ipcnlem1  22984  caucfil  23021  metcld  23044  metcld2  23045  volcn  23314  itg2cnlem2  23469  ellimc2  23581  dveflem  23680  dvne0  23712  mdegleb  23762  mdegle0  23775  ply1divex  23834  fta1g  23865  dgrco  23969  plydivex  23990  fta1  24001  vieta1  24005  abelthlem8  24131  divlogrlim  24315  cxpcn3lem  24422  rlimcnp  24626  cxplim  24632  cxploglim  24638  ftalem1  24733  ftalem2  24734  dvdsmulf1o  24854  ppiublem1  24861  dchrinv  24920  lgseisenlem2  25035  2sqlem6  25082  2sqlem8  25085  2sqlem10  25087  dchrisum0  25143  istrkgc  25287  istrkgb  25288  axtgcgrid  25296  axtg5seg  25298  axtgpasch  25300  axtgeucl  25305  tgcgr4  25360  axlowdimlem15  25770  usgr2wlkneq  26555  usgr2pthlem  26562  friendshipgt3  27144  isnvlem  27353  vacn  27437  nmcvcn  27438  smcnlem  27440  blocni  27548  norm3lemt  27897  isch2  27968  chlimi  27979  omlsii  28150  eigorth  28585  0cnop  28726  0cnfn  28727  idcnop  28728  lnconi  28780  stcltr1i  29021  elat2  29087  funcnv5mpt  29353  xrge0infss  29410  resspos  29486  xrge0tsmsd  29612  qqhcn  29859  qqhucn  29860  esum2d  29978  eulerpartlemgvv  30261  sgn3da  30426  sgnnbi  30430  sgnpbi  30431  axtgupdim2OLD  30506  bnj1145  30822  bnj1171  30829  bnj1172  30830  erdszelem8  30941  mclsval  31221  mclsax  31227  mclsppslem  31241  climuzcnv  31326  poseq  31504  frrlem4  31537  nocvxminlem  31606  ifscgr  31846  idinside  31886  brsegle  31910  trer  32005  filnetlem4  32071  dnicn  32177  bj-ssbjust  32313  bj-ssbequ  32324  bj-ssblem1  32325  bj-ssblem2  32326  bj-ssb1a  32327  bj-ssb1  32328  bj-ssbcom3lem  32345  bj-19.21t  32513  wl-sbrimt  33002  fin2so  33067  ptrecube  33080  poimirlem26  33106  poimirlem27  33107  heicant  33115  mbfresfi  33127  itg2addnc  33135  ftc1anc  33164  filbcmb  33206  sdclem2  33209  fdc  33212  fdc1  33213  rngoidmlem  33406  divrngidl  33498  pridlval  33503  smprngopr  33522  ax12inda  33752  ax12v2-o  33753  isat3  34113  iscvlat2N  34130  psubspset  34549  ldilfset  34913  ldilset  34914  dilfsetN  34958  dilsetN  34959  cdlemefrs29bpre0  35203  cdlemefrs29clN  35206  cdlemefrs32fva  35207  cdlemn11pre  36018  dihord2pre  36033  lpolsetN  36290  aomclem8  37150  hbtlem5  37218  acsfn1p  37289  ifpbi1  37342  ifpbi12  37353  ifpbi13  37354  ntrneik2  37911  ntrneikb  37913  gneispacess2  37965  2sbc6g  38137  sbiota1  38156  uzwo4  38743  fsumiunss  39243  mullimc  39284  limcdm0  39286  mullimcf  39291  constlimc  39292  idlimc  39294  limsupre  39309  limcleqr  39312  addlimc  39316  0ellimcdiv  39317  limsupref  39353  limsupbnd1f  39354  limsupmnf  39389  limsupre2  39393  limsupmnfuzlem  39394  limsupre2mpt  39398  limsupre3  39401  limsupre3mpt  39402  limsupre3uzlem  39403  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvmptfprodlem  39496  wallispilem3  39621  fourierdlem48  39708  fourierdlem87  39747  sge0f1o  39936  sge0iunmptlemre  39969  sge0iunmpt  39972  vonioo  40233  vonicc  40236  bgoldbachlt  41018  tgoldbachlt  41021  bgoldbachltOLD  41025  tgoldbachltOLD  41028  sprsymrelfolem2  41061  ply1mulgsumlem1  41492  ply1mulgsumlem2  41493  elbigo2  41668  elbigo2r  41669  setrecseq  41755  setrec1lem1  41757  aacllem  41880
  Copyright terms: Public domain W3C validator