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

Theorem imbi1d 329
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 236 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 79 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 217 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 79 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 200 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  imbi12d  332  imbi1  335  imim21b  380  pm5.33  917  con3ALT  1025  con3OLD  1028  19.21t  2060  19.21tOLD  2200  axc15  2290  ax12v2OLD  2329  drsb1  2364  ralcom2  3082  raleqf  3110  ralxpxfr2d  3297  alexeqg  3301  mo2icl  3351  sbc19.21g  3468  csbiebg  3521  ralss  3630  r19.37zv  4018  ssuniOLD  4390  intmin4  4435  ssexg  4726  pocl  4955  vtoclr  5075  frsn  5101  fun11  5862  funimass4  6141  dff13  6393  f1mpt  6396  isopolem  6472  oprabid  6553  caovcan  6713  caoftrn  6807  ordunisuc2  6913  tfisi  6927  tfinds  6928  tfindsg  6929  tfindsg2  6930  dfom2  6936  findsg  6962  frxp  7151  dfsmo2  7308  qliftfun  7696  ecoptocl  7701  ecopovtrn  7714  dom2lem  7858  findcard  8061  findcard2  8062  findcard3  8065  fiint  8099  supmo  8218  eqsup  8222  suplub  8226  supisoex  8240  infmo  8261  wemaplem1  8311  wemaplem2  8312  wemapsolem  8315  oemapvali  8441  cantnf  8450  wemapwe  8454  karden  8618  aceq1  8800  zorn2lem1  9178  axrepndlem2  9271  axregndlem2  9281  pwfseqlem4  9340  gruurn  9476  indpi  9585  nqereu  9607  prcdnq  9671  supexpr  9732  ltsosr  9771  supsrlem  9788  supsr  9789  axpre-lttrn  9843  axpre-sup  9846  prodgt0  10719  infm3  10833  prime  11292  raluz  11570  zsupss  11611  uzsupss  11614  xrsupsslem  11967  xrinfmsslem  11968  fz1sbc  12242  ssnn0fi  12603  fi1uzind  13082  brfi1indALT  13085  fi1uzindOLD  13088  brfi1indALTOLD  13091  wrdind  13276  wrd2ind  13277  relexprelg  13574  rtrclreclem3  13596  relexpindlem  13599  relexpind  13600  rtrclind  13601  rexanre  13882  rexico  13889  limsupgle  14004  rlim2lt  14024  rlim3  14025  ello12  14043  ello12r  14044  ello1d  14050  elo12  14054  elo12r  14055  rlimconst  14071  lo1resb  14091  o1resb  14093  rlimcn2  14117  addcn2  14120  mulcn2  14122  reccn2  14123  cn1lem  14124  o1rlimmul  14145  lo1le  14178  caucvgrlem  14199  divrcnv  14371  rpnnen2lem12  14741  sqrt2irr  14765  dfgcd2  15049  exprmfct  15202  isprm5  15205  isprm7  15206  prmdvdsexpr  15215  prmpwdvds  15394  vdwmc2  15469  ramtlecl  15490  ramub  15503  rami  15505  ramcl  15519  firest  15864  mreexexd  16079  mreexexdOLD  16080  acsfn  16091  prslem  16702  ispos  16718  posi  16721  isposd  16726  lubeldm  16752  lubval  16755  glbeldm  16765  glbval  16768  joinval2lem  16779  meetval2lem  16793  pospropd  16905  odlem1  17725  mndodcongi  17733  gexlem1  17765  sylow1lem3  17786  efgredlemb  17930  efgred  17932  frgpnabllem1  18047  isrrg  19057  mplsubglem  19203  mpllsslem  19204  ltbval  19240  opsrval  19243  xrsdsreclb  19560  islindf4  19943  mdetunilem1  20184  mdetunilem3  20186  mdetunilem4  20187  mdetunilem9  20192  chpscmat  20413  chfacffsupp  20427  chfacfscmulfsupp  20430  chfacfpmmulfsupp  20434  istopg  20472  isclo2  20649  neiptoptop  20692  neiptopnei  20693  lmbr  20819  ist0  20881  ist1-2  20908  t1sep2  20930  cmpfi  20968  2ndcdisj  21016  1stccn  21023  iskgen3  21109  ptpjopn  21172  hausdiag  21205  xkopt  21215  ist0-4  21289  isr0  21297  r0sep  21308  fbfinnfr  21402  fmfnfmlem2  21516  fmfnfmlem4  21518  fmfnfm  21519  cnflf  21563  cnfcf  21603  tmdgsum2  21657  tsmsgsum  21699  tsmsres  21704  tsmsf1o  21705  tsmsxplem1  21713  tsmsxp  21715  ustssel  21766  ustincl  21768  ustdiag  21769  ustinvel  21770  ustexhalf  21771  ust0  21780  ustuqtop4  21805  utopsnneiplem  21808  isucn2  21840  iducn  21844  metcnp  22103  metcnpi3  22108  txmetcnp  22109  metucn  22133  ngptgp  22197  nlmvscnlem1  22247  nrginvrcnlem  22252  nghmcn  22306  xrge0tsms  22392  xmetdcn2  22395  metdscn  22414  addcnlem  22422  elcncf1di  22453  ipcnlem1  22796  caucfil  22833  metcld  22856  metcld2  22857  volcn  23124  itg2cnlem2  23279  ellimc2  23391  dveflem  23490  dvne0  23522  mdegleb  23572  mdegle0  23585  ply1divex  23644  fta1g  23675  dgrco  23779  plydivex  23800  fta1  23811  vieta1  23815  abelthlem8  23941  divlogrlim  24125  cxpcn3lem  24232  rlimcnp  24436  cxplim  24442  cxploglim  24448  ftalem1  24543  ftalem2  24544  dvdsmulf1o  24664  ppiublem1  24671  dchrinv  24730  lgseisenlem2  24845  2sqlem6  24892  2sqlem8  24895  2sqlem10  24897  dchrisum0  24953  istrkgc  25097  istrkgb  25098  axtgcgrid  25106  axtg5seg  25108  axtgpasch  25110  axtgeucl  25115  tgcgr4  25171  axlowdimlem15  25581  usgra2wlkspthlem1  25940  usgra2wlkspthlem2  25941  3v3e3cycl1  25965  constr3trllem2  25972  4cycl4v4e  25987  4cycl4dv4e  25989  eupatrl  26288  frgrawopreglem2  26365  usg2spot2nb  26385  friendshipgt3  26441  isnvlem  26642  vacn  26726  nmcvcn  26727  smcnlem  26729  blocni  26837  norm3lemt  27186  isch2  27257  chlimi  27268  omlsii  27439  eigorth  27874  0cnop  28015  0cnfn  28016  idcnop  28017  lnconi  28069  stcltr1i  28310  elat2  28376  funcnv5mpt  28645  xrge0infss  28708  resspos  28783  xrge0tsmsd  28909  qqhcn  29156  qqhucn  29157  esum2d  29275  eulerpartlemgvv  29558  sgn3da  29723  sgnnbi  29727  sgnpbi  29728  axtgupdim2OLD  29792  bnj1145  30108  bnj1171  30115  bnj1172  30116  erdszelem8  30227  mclsval  30507  mclsax  30513  mclsppslem  30527  climuzcnv  30612  poseq  30787  frrlem4  30820  nocvxminlem  30882  ifscgr  31114  idinside  31154  brsegle  31178  trer  31273  filnetlem4  31339  dnicn  31445  bj-ssbequ  31611  bj-ssblem1  31612  bj-ssblem2  31613  bj-ssb1a  31614  bj-ssb1  31615  bj-ssbcom3lem  31632  bj-19.21t  31798  wl-sbrimt  32293  fin2so  32349  ptrecube  32362  poimirlem26  32388  poimirlem27  32389  heicant  32397  mbfresfi  32409  itg2addnc  32417  ftc1anc  32446  filbcmb  32488  sdclem2  32491  fdc  32494  fdc1  32495  rngoidmlem  32688  divrngidl  32780  pridlval  32785  smprngopr  32804  ax12inda  33034  ax12v2-o  33035  isat3  33395  iscvlat2N  33412  psubspset  33831  ldilfset  34195  ldilset  34196  dilfsetN  34240  dilsetN  34241  cdlemefrs29bpre0  34485  cdlemefrs29clN  34488  cdlemefrs32fva  34489  cdlemn11pre  35300  dihord2pre  35315  lpolsetN  35572  aomclem8  36432  hbtlem5  36500  acsfn1p  36571  ifpbi1  36624  ifpbi12  36635  ifpbi13  36636  ntrneik2  37193  ntrneikb  37195  gneispacess2  37247  2sbc6g  37421  sbiota1  37440  uzwo4  38029  fsumiunss  38425  mullimc  38466  limcdm0  38468  mullimcf  38473  constlimc  38474  idlimc  38476  limsupre  38491  limcleqr  38494  addlimc  38498  0ellimcdiv  38499  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvmptfprodlem  38617  wallispilem3  38743  fourierdlem48  38830  fourierdlem87  38869  sge0f1o  39058  sge0iunmptlemre  39091  sge0iunmpt  39094  vonioo  39356  vonicc  39359  bgoldbachlt  40011  tgoldbachlt  40014  bgoldbachltOLD  40018  tgoldbachltOLD  40021  usgr2wlkneq  40943  usgr2pthlem  40950  av-friendshipgt3  41533  ply1mulgsumlem1  41949  ply1mulgsumlem2  41950  elbigo2  42125  elbigo2r  42126  aacllem  42298
  Copyright terms: Public domain W3C validator