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

Theorem imbi1d 345
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 251 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 82 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 232 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 82 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 215 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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
This theorem is referenced by:  imbi12d  348  imbi1  351  imim21b  398  pm5.33  834  con3ALT  1082  norasslem3  1533  sbjust  2068  sbequ  2089  sb6  2091  19.21t  2205  sb4b  2491  sb4bOLD  2492  drsb1  2516  ralcom2  3319  raleqf  3353  rspceaimv  3579  ralxpxfr2d  3590  alexeqg  3595  mo2icl  3656  sbc19.21g  3795  csbiebg  3863  ralss  3988  r19.37zv  4408  reuprg0  4601  intmin4  4870  ssexg  5194  pocl  5449  vtoclr  5583  frsn  5607  fun11  6402  funimass4  6709  dff13  6995  f1mpt  7001  isopolem  7081  oprabidw  7170  oprabid  7171  caovcan  7336  caoftrn  7428  ordunisuc2  7543  tfisi  7557  tfinds  7558  tfindsg  7559  tfindsg2  7560  dfom2  7566  findsg  7594  frxp  7807  dfsmo2  7971  qliftfun  8369  ecoptocl  8374  ecopovtrn  8387  dom2lem  8536  findcard  8745  findcard2  8746  findcard3  8749  fiint  8783  supmo  8904  eqsup  8908  suplub  8912  supisoex  8926  infmo  8947  wemaplem1  8998  wemaplem2  8999  wemapsolem  9002  oemapvali  9135  cantnf  9144  wemapwe  9148  karden  9312  aceq1  9532  zorn2lem1  9911  axrepndlem2  10008  axregndlem2  10018  pwfseqlem4  10077  gruurn  10213  indpi  10322  nqereu  10344  prcdnq  10408  supexpr  10469  ltsosr  10509  supsrlem  10526  supsr  10527  axpre-lttrn  10581  axpre-sup  10584  prodgt0  11480  infm3  11591  prime  12055  raluz  12288  zsupss  12329  uzsupss  12332  xrsupsslem  12692  xrinfmsslem  12693  fz1sbc  12982  ssnn0fi  13352  fi1uzind  13855  brfi1indALT  13858  wrdind  14079  wrd2ind  14080  relexprelg  14393  rtrclreclem3  14415  relexpindlem  14418  relexpind  14419  rtrclind  14420  rexanre  14702  rexico  14709  reusq0  14818  limsupgle  14830  ello12  14869  ello12r  14870  ello1d  14876  elo12  14880  elo12r  14881  lo1resb  14917  o1resb  14919  rlimcn2  14943  addcn2  14946  mulcn2  14948  lo1le  15004  rpnnen2lem12  15574  sqrt2irr  15598  dfgcd2  15888  exprmfct  16042  isprm5  16045  isprm7  16046  prmdvdsexpr  16055  prmpwdvds  16234  vdwmc2  16309  ramtlecl  16330  ramub  16343  rami  16345  ramcl  16359  firest  16702  mreexexd  16915  acsfn  16926  prslem  17537  ispos  17553  posi  17556  isposd  17561  lubeldm  17587  lubval  17590  glbeldm  17600  glbval  17603  joinval2lem  17614  meetval2lem  17628  pospropd  17740  odlem1  18659  mndodcongi  18667  gexlem1  18700  sylow1lem3  18721  efgredlemb  18868  efgred  18870  frgpnabllem1  18990  acsfn1p  19575  isrrg  20058  xrsdsreclb  20142  islindf4  20531  mplsubglem  20676  mpllsslem  20677  ltbval  20715  opsrval  20718  mdetunilem1  21221  mdetunilem3  21223  mdetunilem4  21224  mdetunilem9  21229  chpscmat  21451  istopg  21504  isclo2  21697  neiptoptop  21740  neiptopnei  21741  lmbr  21867  ist0  21929  ist1-2  21956  t1sep2  21978  cmpfi  22017  2ndcdisj  22065  1stccn  22072  iskgen3  22158  ptpjopn  22221  hausdiag  22254  xkopt  22264  ist0-4  22338  isr0  22346  r0sep  22357  fbfinnfr  22450  fmfnfmlem2  22564  fmfnfmlem4  22566  fmfnfm  22567  cnflf  22611  cnfcf  22651  tmdgsum2  22705  tsmsf1o  22754  tsmsxplem1  22762  ustssel  22815  ustincl  22817  ustdiag  22818  ustinvel  22819  ustexhalf  22820  ust0  22829  ustuqtop4  22854  utopsnneiplem  22857  isucn2  22889  iducn  22893  metcnp  23152  txmetcnp  23158  metucn  23182  ngptgp  23246  nlmvscnlem1  23296  xrge0tsms  23443  xmetdcn2  23446  addcnlem  23473  ipcnlem1  23853  caucfil  23891  metcld  23914  metcld2  23915  ellimc2  24484  dvne0  24618  mdegleb  24669  mdegle0  24682  ply1divex  24741  fta1g  24772  dgrco  24876  plydivex  24897  fta1  24908  vieta1  24912  cxpcn3lem  25340  rlimcnp  25555  dvdsmulf1o  25783  ppiublem1  25790  dchrinv  25849  lgseisenlem2  25964  2sqlem6  26011  2sqlem8  26014  2sqlem10  26016  istrkgc  26252  istrkgb  26253  axtgcgrid  26261  axtg5seg  26263  axtgpasch  26265  axtgeucl  26270  tgcgr4  26329  axlowdimlem15  26754  usgr2wlkneq  27549  usgr2pthlem  27556  friendshipgt3  28187  isnvlem  28397  vacn  28481  smcnlem  28484  norm3lemt  28939  isch2  29010  chlimi  29021  omlsii  29190  eigorth  29625  stcltr1i  30061  elat2  30127  funcnv5mpt  30435  xrge0infss  30514  wrdt2ind  30657  resspos  30676  xrge0tsmsd  30746  islinds5  30987  prmidlval  31024  ist0cld  31190  qqhucn  31347  esum2d  31466  eulerpartlemgvv  31748  sgn3da  31913  sgnnbi  31917  sgnpbi  31918  tgoldbachgt  32048  axtgupdim2ALTV  32053  bnj1145  32379  bnj1171  32386  bnj1172  32387  isacycgr1  32507  acycgrcycl  32508  erdszelem8  32559  satfrnmapom  32731  mclsval  32924  mclsax  32930  mclsppslem  32944  climuzcnv  33028  elintfv  33121  poseq  33209  frrlem12  33248  nocvxminlem  33361  ifscgr  33619  idinside  33659  brsegle  33683  trer  33778  filnetlem4  33843  bj-ssblem1  34101  bj-ssblem2  34102  bj-ax12  34104  bj-19.21t0  34269  mobidvALT  34297  currysetlem  34381  currysetlem1  34383  wl-sbrimt  34950  wl-dfralflem  35002  fin2so  35043  ptrecube  35056  poimirlem26  35082  poimirlem27  35083  heicant  35091  mbfresfi  35102  itg2addnc  35110  filbcmb  35177  sdclem2  35179  fdc  35182  fdc1  35183  rngoidmlem  35373  divrngidl  35465  pridlval  35470  smprngopr  35489  inecmo  35768  elcnvrefrels3  35930  ax12inda  36243  ax12v2-o  36244  isat3  36602  iscvlat2N  36619  psubspset  37039  ldilfset  37403  ldilset  37404  dilfsetN  37447  dilsetN  37448  cdlemefrs29bpre0  37691  cdlemefrs29clN  37694  cdlemefrs32fva  37695  cdlemn11pre  38505  dihord2pre  38520  lpolsetN  38777  fsuppind  39449  aomclem8  39998  hbtlem5  40065  ifpbi1  40178  ifpbi12  40189  ifpbi13  40190  ntrneik2  40788  ntrneikb  40790  gneispacess2  40842  2sbc6g  41112  sbiota1  41131  uzwo4  41680  fsumiunss  42210  limsupre  42276  limsupref  42320  limsupbnd1f  42321  limsupmnf  42356  limsupre2  42360  limsupmnfuzlem  42361  limsupre2mpt  42365  limsupre3  42368  limsupre3mpt  42369  ioodvbdlimc1lem2  42567  ioodvbdlimc2lem  42569  dvmptfprodlem  42579  wallispilem3  42702  fourierdlem48  42789  sge0f1o  43014  sge0iunmptlemre  43047  sge0iunmpt  43050  vonioo  43314  vonicc  43317  2reu8i  43662  2reuimp0  43663  2reuimp  43664  sprsymrelfolem2  44003  paireqne  44021  nfermltlrev  44255  bgoldbachlt  44324  tgoldbachlt  44327  ply1mulgsumlem1  44787  ply1mulgsumlem2  44788  elbigo2  44959  elbigo2r  44960  setrecseq  45208  setrec1lem1  45210  aacllem  45322
  Copyright terms: Public domain W3C validator