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

Theorem imbi1d 330
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  333  imbi1  336  imim21b  381  pm5.33  958  con3ALT  1070  19.21t  2218  19.21tOLDOLD  2219  19.21tOLD  2356  axc15  2446  drsb1  2512  ralcom2  3240  raleqf  3271  ralxpxfr2d  3464  alexeqg  3469  mo2icl  3524  sbc19.21g  3641  csbiebg  3695  ralss  3807  r19.37zv  4209  ssuniOLD  4610  intmin4  4656  ssexg  4954  pocl  5192  vtoclr  5319  frsn  5344  fun11  6122  funimass4  6407  dff13  6673  f1mpt  6679  isopolem  6756  oprabid  6838  caovcan  7001  caoftrn  7095  ordunisuc2  7207  tfisi  7221  tfinds  7222  tfindsg  7223  tfindsg2  7224  dfom2  7230  findsg  7256  frxp  7453  dfsmo2  7611  qliftfun  7997  ecoptocl  8002  ecopovtrn  8015  dom2lem  8159  findcard  8362  findcard2  8363  findcard3  8366  fiint  8400  supmo  8521  eqsup  8525  suplub  8529  supisoex  8543  infmo  8564  wemaplem1  8614  wemaplem2  8615  wemapsolem  8618  oemapvali  8752  cantnf  8761  wemapwe  8765  karden  8929  aceq1  9128  zorn2lem1  9508  axrepndlem2  9605  axregndlem2  9615  pwfseqlem4  9674  gruurn  9810  indpi  9919  nqereu  9941  prcdnq  10005  supexpr  10066  ltsosr  10105  supsrlem  10122  supsr  10123  axpre-lttrn  10177  axpre-sup  10180  prodgt0  11058  infm3  11172  prime  11648  raluz  11927  zsupss  11968  uzsupss  11971  xrsupsslem  12328  xrinfmsslem  12329  fz1sbc  12607  ssnn0fi  12976  fi1uzind  13469  brfi1indALT  13472  wrdind  13674  wrd2ind  13675  relexprelg  13975  rtrclreclem3  13997  relexpindlem  14000  relexpind  14001  rtrclind  14002  rexanre  14283  rexico  14290  limsupgle  14405  rlim2lt  14425  rlim3  14426  ello12  14444  ello12r  14445  ello1d  14451  elo12  14455  elo12r  14456  rlimconst  14472  lo1resb  14492  o1resb  14494  rlimcn2  14518  addcn2  14521  mulcn2  14523  reccn2  14524  cn1lem  14525  o1rlimmul  14546  lo1le  14579  caucvgrlem  14600  divrcnv  14781  rpnnen2lem12  15151  sqrt2irr  15176  dfgcd2  15463  exprmfct  15616  isprm5  15619  isprm7  15620  prmdvdsexpr  15629  prmpwdvds  15808  vdwmc2  15883  ramtlecl  15904  ramub  15917  rami  15919  ramcl  15933  firest  16293  mreexexd  16508  acsfn  16519  prslem  17130  ispos  17146  posi  17149  isposd  17154  lubeldm  17180  lubval  17183  glbeldm  17193  glbval  17196  joinval2lem  17207  meetval2lem  17221  pospropd  17333  odlem1  18152  mndodcongi  18160  gexlem1  18192  sylow1lem3  18213  efgredlemb  18357  efgred  18359  frgpnabllem1  18474  isrrg  19488  mplsubglem  19634  mpllsslem  19635  ltbval  19671  opsrval  19674  xrsdsreclb  19993  islindf4  20377  mdetunilem1  20618  mdetunilem3  20620  mdetunilem4  20621  mdetunilem9  20626  chpscmat  20847  chfacffsupp  20861  chfacfscmulfsupp  20864  chfacfpmmulfsupp  20868  istopg  20900  isclo2  21092  neiptoptop  21135  neiptopnei  21136  lmbr  21262  ist0  21324  ist1-2  21351  t1sep2  21373  cmpfi  21411  2ndcdisj  21459  1stccn  21466  iskgen3  21552  ptpjopn  21615  hausdiag  21648  xkopt  21658  ist0-4  21732  isr0  21740  r0sep  21751  fbfinnfr  21844  fmfnfmlem2  21958  fmfnfmlem4  21960  fmfnfm  21961  cnflf  22005  cnfcf  22045  tmdgsum2  22099  tsmsgsum  22141  tsmsres  22146  tsmsf1o  22147  tsmsxplem1  22155  tsmsxp  22157  ustssel  22208  ustincl  22210  ustdiag  22211  ustinvel  22212  ustexhalf  22213  ust0  22222  ustuqtop4  22247  utopsnneiplem  22250  isucn2  22282  iducn  22286  metcnp  22545  metcnpi3  22550  txmetcnp  22551  metucn  22575  ngptgp  22639  nlmvscnlem1  22689  nrginvrcnlem  22694  nghmcn  22748  xrge0tsms  22836  xmetdcn2  22839  metdscn  22858  addcnlem  22866  elcncf1di  22897  ipcnlem1  23242  caucfil  23279  metcld  23302  metcld2  23303  volcn  23572  itg2cnlem2  23726  ellimc2  23838  dveflem  23939  dvne0  23971  mdegleb  24021  mdegle0  24034  ply1divex  24093  fta1g  24124  dgrco  24228  plydivex  24249  fta1  24260  vieta1  24264  abelthlem8  24390  divlogrlim  24578  cxpcn3lem  24685  rlimcnp  24889  cxplim  24895  cxploglim  24901  ftalem1  24996  ftalem2  24997  dvdsmulf1o  25117  ppiublem1  25124  dchrinv  25183  lgseisenlem2  25298  2sqlem6  25345  2sqlem8  25348  2sqlem10  25350  dchrisum0  25406  istrkgc  25550  istrkgb  25551  axtgcgrid  25559  axtg5seg  25561  axtgpasch  25563  axtgeucl  25568  tgcgr4  25623  axlowdimlem15  26033  usgr2wlkneq  26860  usgr2pthlem  26867  friendshipgt3  27564  isnvlem  27772  vacn  27856  nmcvcn  27857  smcnlem  27859  blocni  27967  norm3lemt  28316  isch2  28387  chlimi  28398  omlsii  28569  eigorth  29004  0cnop  29145  0cnfn  29146  idcnop  29147  lnconi  29199  stcltr1i  29440  elat2  29506  funcnv5mpt  29776  xrge0infss  29832  resspos  29966  xrge0tsmsd  30092  qqhcn  30342  qqhucn  30343  esum2d  30462  eulerpartlemgvv  30745  sgn3da  30910  sgnnbi  30914  sgnpbi  30915  tgoldbachgt  31048  axtgupdim2OLD  31053  bnj1145  31366  bnj1171  31373  bnj1172  31374  erdszelem8  31485  mclsval  31765  mclsax  31771  mclsppslem  31785  climuzcnv  31870  elintfv  31967  poseq  32057  nocvxminlem  32197  ifscgr  32455  idinside  32495  brsegle  32519  trer  32614  filnetlem4  32680  dnicn  32786  bj-ssbjust  32922  bj-ssbequ  32933  bj-ssblem1  32934  bj-ssblem2  32935  bj-ssb1a  32936  bj-ssb1  32937  bj-ssbcom3lem  32954  bj-19.21t  33121  wl-sbrimt  33642  fin2so  33707  ptrecube  33720  poimirlem26  33746  poimirlem27  33747  heicant  33755  mbfresfi  33767  itg2addnc  33775  ftc1anc  33804  filbcmb  33846  sdclem2  33849  fdc  33852  fdc1  33853  rngoidmlem  34046  divrngidl  34138  pridlval  34143  smprngopr  34162  inecmo  34441  elcnvrefrels3  34602  ax12inda  34735  ax12v2-o  34736  isat3  35095  iscvlat2N  35112  psubspset  35531  ldilfset  35895  ldilset  35896  dilfsetN  35940  dilsetN  35941  cdlemefrs29bpre0  36184  cdlemefrs29clN  36187  cdlemefrs32fva  36188  cdlemn11pre  36999  dihord2pre  37014  lpolsetN  37271  aomclem8  38131  hbtlem5  38198  acsfn1p  38269  ifpbi1  38322  ifpbi12  38333  ifpbi13  38334  ntrneik2  38890  ntrneikb  38892  gneispacess2  38944  2sbc6g  39116  sbiota1  39135  uzwo4  39718  fsumiunss  40308  mullimc  40349  limcdm0  40351  mullimcf  40356  constlimc  40357  idlimc  40359  limsupre  40374  limcleqr  40377  addlimc  40381  0ellimcdiv  40382  limsupref  40418  limsupbnd1f  40419  limsupmnf  40454  limsupre2  40458  limsupmnfuzlem  40459  limsupre2mpt  40463  limsupre3  40466  limsupre3mpt  40467  limsupre3uzlem  40468  ioodvbdlimc1lem2  40648  ioodvbdlimc2lem  40650  dvmptfprodlem  40660  wallispilem3  40785  fourierdlem48  40872  fourierdlem87  40911  sge0f1o  41100  sge0iunmptlemre  41133  sge0iunmpt  41136  vonioo  41400  vonicc  41403  bgoldbachlt  42209  tgoldbachlt  42212  bgoldbachltOLD  42215  tgoldbachltOLD  42218  sprsymrelfolem2  42251  ply1mulgsumlem1  42682  ply1mulgsumlem2  42683  elbigo2  42854  elbigo2r  42855  setrecseq  42940  setrec1lem1  42942  aacllem  43058
  Copyright terms: Public domain W3C validator