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

Theorem imbi1d 343
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 249 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 82 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 230 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 82 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 213 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  imbi12d  346  imbi1  349  imim21b  395  pm5.33  831  con3ALT  1076  con3ALTOLD  1077  norasslem3  1523  sbjust  2059  sbequ  2081  sb6  2084  19.21t  2196  axc15OLD  2436  sb4b  2492  sb4bOLD  2493  drsb1  2528  ralcom2w  3360  ralcom2  3361  raleqf  3395  rspceaimv  3625  ralxpxfr2d  3636  alexeqg  3641  mo2icl  3702  sbc19.21g  3843  csbiebg  3912  ralss  4034  r19.37zv  4443  reuprg0  4630  intmin4  4896  ssexg  5218  pocl  5474  vtoclr  5608  frsn  5632  fun11  6421  funimass4  6723  dff13  7004  f1mpt  7010  isopolem  7087  oprabidw  7176  oprabid  7177  caovcan  7341  caoftrn  7433  ordunisuc2  7548  tfisi  7562  tfinds  7563  tfindsg  7564  tfindsg2  7565  dfom2  7571  findsg  7598  frxp  7809  dfsmo2  7973  qliftfun  8371  ecoptocl  8376  ecopovtrn  8389  dom2lem  8537  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  9531  zorn2lem1  9906  axrepndlem2  10003  axregndlem2  10013  pwfseqlem4  10072  gruurn  10208  indpi  10317  nqereu  10339  prcdnq  10403  supexpr  10464  ltsosr  10504  supsrlem  10521  supsr  10522  axpre-lttrn  10576  axpre-sup  10579  prodgt0  11475  infm3  11588  prime  12051  raluz  12284  zsupss  12325  uzsupss  12328  xrsupsslem  12688  xrinfmsslem  12689  fz1sbc  12971  ssnn0fi  13341  fi1uzind  13843  brfi1indALT  13846  wrdind  14072  wrd2ind  14073  relexprelg  14385  rtrclreclem3  14407  relexpindlem  14410  relexpind  14411  rtrclind  14412  rexanre  14694  rexico  14701  reusq0  14810  limsupgle  14822  ello12  14861  ello12r  14862  ello1d  14868  elo12  14872  elo12r  14873  lo1resb  14909  o1resb  14911  rlimcn2  14935  addcn2  14938  mulcn2  14940  lo1le  14996  rpnnen2lem12  15566  sqrt2irr  15590  dfgcd2  15882  exprmfct  16036  isprm5  16039  isprm7  16040  prmdvdsexpr  16049  prmpwdvds  16228  vdwmc2  16303  ramtlecl  16324  ramub  16337  rami  16339  ramcl  16353  firest  16694  mreexexd  16907  acsfn  16918  prslem  17529  ispos  17545  posi  17548  isposd  17553  lubeldm  17579  lubval  17582  glbeldm  17592  glbval  17595  joinval2lem  17606  meetval2lem  17620  pospropd  17732  odlem1  18592  mndodcongi  18600  gexlem1  18633  sylow1lem3  18654  efgredlemb  18801  efgred  18803  frgpnabllem1  18922  acsfn1p  19507  isrrg  19989  mplsubglem  20142  mpllsslem  20143  ltbval  20180  opsrval  20183  xrsdsreclb  20520  islindf4  20910  mdetunilem1  21149  mdetunilem3  21151  mdetunilem4  21152  mdetunilem9  21157  chpscmat  21378  istopg  21431  isclo2  21624  neiptoptop  21667  neiptopnei  21668  lmbr  21794  ist0  21856  ist1-2  21883  t1sep2  21905  cmpfi  21944  2ndcdisj  21992  1stccn  21999  iskgen3  22085  ptpjopn  22148  hausdiag  22181  xkopt  22191  ist0-4  22265  isr0  22273  r0sep  22284  fbfinnfr  22377  fmfnfmlem2  22491  fmfnfmlem4  22493  fmfnfm  22494  cnflf  22538  cnfcf  22578  tmdgsum2  22632  tsmsf1o  22680  tsmsxplem1  22688  ustssel  22741  ustincl  22743  ustdiag  22744  ustinvel  22745  ustexhalf  22746  ust0  22755  ustuqtop4  22780  utopsnneiplem  22783  isucn2  22815  iducn  22819  metcnp  23078  txmetcnp  23084  metucn  23108  ngptgp  23172  nlmvscnlem1  23222  xrge0tsms  23369  xmetdcn2  23372  addcnlem  23399  ipcnlem1  23775  caucfil  23813  metcld  23836  metcld2  23837  ellimc2  24402  dvne0  24535  mdegleb  24585  mdegle0  24598  ply1divex  24657  fta1g  24688  dgrco  24792  plydivex  24813  fta1  24824  vieta1  24828  cxpcn3lem  25255  rlimcnp  25470  dvdsmulf1o  25698  ppiublem1  25705  dchrinv  25764  lgseisenlem2  25879  2sqlem6  25926  2sqlem8  25929  2sqlem10  25931  istrkgc  26167  istrkgb  26168  axtgcgrid  26176  axtg5seg  26178  axtgpasch  26180  axtgeucl  26185  tgcgr4  26244  axlowdimlem15  26669  usgr2wlkneq  27464  usgr2pthlem  27471  friendshipgt3  28104  isnvlem  28314  vacn  28398  smcnlem  28401  norm3lemt  28856  isch2  28927  chlimi  28938  omlsii  29107  eigorth  29542  stcltr1i  29978  elat2  30044  funcnv5mpt  30341  xrge0infss  30410  wrdt2ind  30554  resspos  30573  xrge0tsmsd  30619  islinds5  30859  prmidlval  30873  qqhucn  31132  esum2d  31251  eulerpartlemgvv  31533  sgn3da  31698  sgnnbi  31702  sgnpbi  31703  tgoldbachgt  31833  axtgupdim2ALTV  31838  bnj1145  32162  bnj1171  32169  bnj1172  32170  isacycgr1  32290  acycgrcycl  32291  erdszelem8  32342  satfrnmapom  32514  mclsval  32707  mclsax  32713  mclsppslem  32727  climuzcnv  32811  elintfv  32904  poseq  32992  frrlem12  33031  nocvxminlem  33144  ifscgr  33402  idinside  33442  brsegle  33466  trer  33561  filnetlem4  33626  bj-ssblem1  33884  bj-ssblem2  33885  bj-ax12  33887  bj-19.21t0  34050  mobidvALT  34078  currysetlem  34153  currysetlem1  34155  wl-sbrimt  34667  wl-dfralflem  34719  fin2so  34760  ptrecube  34773  poimirlem26  34799  poimirlem27  34800  heicant  34808  mbfresfi  34819  itg2addnc  34827  filbcmb  34896  sdclem2  34898  fdc  34901  fdc1  34902  rngoidmlem  35095  divrngidl  35187  pridlval  35192  smprngopr  35211  inecmo  35490  elcnvrefrels3  35651  ax12inda  35964  ax12v2-o  35965  isat3  36323  iscvlat2N  36340  psubspset  36760  ldilfset  37124  ldilset  37125  dilfsetN  37168  dilsetN  37169  cdlemefrs29bpre0  37412  cdlemefrs29clN  37415  cdlemefrs32fva  37416  cdlemn11pre  38226  dihord2pre  38241  lpolsetN  38498  aomclem8  39539  hbtlem5  39606  ifpbi1  39721  ifpbi12  39732  ifpbi13  39733  ntrneik2  40320  ntrneikb  40322  gneispacess2  40374  2sbc6g  40624  sbiota1  40643  uzwo4  41192  fsumiunss  41732  limsupre  41798  limsupref  41842  limsupbnd1f  41843  limsupmnf  41878  limsupre2  41882  limsupmnfuzlem  41883  limsupre2mpt  41887  limsupre3  41890  limsupre3mpt  41891  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvmptfprodlem  42105  wallispilem3  42229  fourierdlem48  42316  sge0f1o  42541  sge0iunmptlemre  42574  sge0iunmpt  42577  vonioo  42841  vonicc  42844  2reu8i  43189  2reuimp0  43190  2reuimp  43191  sprsymrelfolem2  43532  paireqne  43550  nfermltlrev  43786  bgoldbachlt  43855  tgoldbachlt  43858  ply1mulgsumlem1  44368  ply1mulgsumlem2  44369  elbigo2  44540  elbigo2r  44541  setrecseq  44716  setrec1lem1  44718  aacllem  44830
  Copyright terms: Public domain W3C validator