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  940  con3ALT  1052  19.21t  2111  19.21tOLDOLD  2112  19.21tOLD  2249  axc15  2339  drsb1  2405  ralcom2  3133  raleqf  3164  ralxpxfr2d  3358  alexeqg  3363  mo2icl  3418  sbc19.21g  3535  csbiebg  3589  ralss  3701  r19.37zv  4100  ssuniOLD  4492  intmin4  4538  ssexg  4837  pocl  5071  vtoclr  5198  frsn  5223  fun11  6001  funimass4  6286  dff13  6552  f1mpt  6558  isopolem  6635  oprabid  6717  caovcan  6880  caoftrn  6974  ordunisuc2  7086  tfisi  7100  tfinds  7101  tfindsg  7102  tfindsg2  7103  dfom2  7109  findsg  7135  frxp  7332  dfsmo2  7489  qliftfun  7875  ecoptocl  7880  ecopovtrn  7893  dom2lem  8037  findcard  8240  findcard2  8241  findcard3  8244  fiint  8278  supmo  8399  eqsup  8403  suplub  8407  supisoex  8421  infmo  8442  wemaplem1  8492  wemaplem2  8493  wemapsolem  8496  oemapvali  8619  cantnf  8628  wemapwe  8632  karden  8796  aceq1  8978  zorn2lem1  9356  axrepndlem2  9453  axregndlem2  9463  pwfseqlem4  9522  gruurn  9658  indpi  9767  nqereu  9789  prcdnq  9853  supexpr  9914  ltsosr  9953  supsrlem  9970  supsr  9971  axpre-lttrn  10025  axpre-sup  10028  prodgt0  10906  infm3  11020  prime  11496  raluz  11774  zsupss  11815  uzsupss  11818  xrsupsslem  12175  xrinfmsslem  12176  fz1sbc  12454  ssnn0fi  12824  fi1uzind  13317  brfi1indALT  13320  wrdind  13522  wrd2ind  13523  relexprelg  13822  rtrclreclem3  13844  relexpindlem  13847  relexpind  13848  rtrclind  13849  rexanre  14130  rexico  14137  limsupgle  14252  rlim2lt  14272  rlim3  14273  ello12  14291  ello12r  14292  ello1d  14298  elo12  14302  elo12r  14303  rlimconst  14319  lo1resb  14339  o1resb  14341  rlimcn2  14365  addcn2  14368  mulcn2  14370  reccn2  14371  cn1lem  14372  o1rlimmul  14393  lo1le  14426  caucvgrlem  14447  divrcnv  14628  rpnnen2lem12  14998  sqrt2irr  15023  dfgcd2  15310  exprmfct  15463  isprm5  15466  isprm7  15467  prmdvdsexpr  15476  prmpwdvds  15655  vdwmc2  15730  ramtlecl  15751  ramub  15764  rami  15766  ramcl  15780  firest  16140  mreexexd  16355  mreexexdOLD  16356  acsfn  16367  prslem  16978  ispos  16994  posi  16997  isposd  17002  lubeldm  17028  lubval  17031  glbeldm  17041  glbval  17044  joinval2lem  17055  meetval2lem  17069  pospropd  17181  odlem1  18000  mndodcongi  18008  gexlem1  18040  sylow1lem3  18061  efgredlemb  18205  efgred  18207  frgpnabllem1  18322  isrrg  19336  mplsubglem  19482  mpllsslem  19483  ltbval  19519  opsrval  19522  xrsdsreclb  19841  islindf4  20225  mdetunilem1  20466  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  chpscmat  20695  chfacffsupp  20709  chfacfscmulfsupp  20712  chfacfpmmulfsupp  20716  istopg  20748  isclo2  20940  neiptoptop  20983  neiptopnei  20984  lmbr  21110  ist0  21172  ist1-2  21199  t1sep2  21221  cmpfi  21259  2ndcdisj  21307  1stccn  21314  iskgen3  21400  ptpjopn  21463  hausdiag  21496  xkopt  21506  ist0-4  21580  isr0  21588  r0sep  21599  fbfinnfr  21692  fmfnfmlem2  21806  fmfnfmlem4  21808  fmfnfm  21809  cnflf  21853  cnfcf  21893  tmdgsum2  21947  tsmsgsum  21989  tsmsres  21994  tsmsf1o  21995  tsmsxplem1  22003  tsmsxp  22005  ustssel  22056  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ust0  22070  ustuqtop4  22095  utopsnneiplem  22098  isucn2  22130  iducn  22134  metcnp  22393  metcnpi3  22398  txmetcnp  22399  metucn  22423  ngptgp  22487  nlmvscnlem1  22537  nrginvrcnlem  22542  nghmcn  22596  xrge0tsms  22684  xmetdcn2  22687  metdscn  22706  addcnlem  22714  elcncf1di  22745  ipcnlem1  23090  caucfil  23127  metcld  23150  metcld2  23151  volcn  23420  itg2cnlem2  23574  ellimc2  23686  dveflem  23787  dvne0  23819  mdegleb  23869  mdegle0  23882  ply1divex  23941  fta1g  23972  dgrco  24076  plydivex  24097  fta1  24108  vieta1  24112  abelthlem8  24238  divlogrlim  24426  cxpcn3lem  24533  rlimcnp  24737  cxplim  24743  cxploglim  24749  ftalem1  24844  ftalem2  24845  dvdsmulf1o  24965  ppiublem1  24972  dchrinv  25031  lgseisenlem2  25146  2sqlem6  25193  2sqlem8  25196  2sqlem10  25198  dchrisum0  25254  istrkgc  25398  istrkgb  25399  axtgcgrid  25407  axtg5seg  25409  axtgpasch  25411  axtgeucl  25416  tgcgr4  25471  axlowdimlem15  25881  usgr2wlkneq  26708  usgr2pthlem  26715  friendshipgt3  27385  isnvlem  27593  vacn  27677  nmcvcn  27678  smcnlem  27680  blocni  27788  norm3lemt  28137  isch2  28208  chlimi  28219  omlsii  28390  eigorth  28825  0cnop  28966  0cnfn  28967  idcnop  28968  lnconi  29020  stcltr1i  29261  elat2  29327  funcnv5mpt  29597  xrge0infss  29653  resspos  29787  xrge0tsmsd  29913  qqhcn  30163  qqhucn  30164  esum2d  30283  eulerpartlemgvv  30566  sgn3da  30731  sgnnbi  30735  sgnpbi  30736  tgoldbachgt  30869  axtgupdim2OLD  30874  bnj1145  31187  bnj1171  31194  bnj1172  31195  erdszelem8  31306  mclsval  31586  mclsax  31592  mclsppslem  31606  climuzcnv  31691  elintfv  31788  poseq  31878  nocvxminlem  32018  ifscgr  32276  idinside  32316  brsegle  32340  trer  32435  filnetlem4  32501  dnicn  32607  bj-ssbjust  32743  bj-ssbequ  32754  bj-ssblem1  32755  bj-ssblem2  32756  bj-ssb1a  32757  bj-ssb1  32758  bj-ssbcom3lem  32775  bj-19.21t  32942  wl-sbrimt  33461  fin2so  33526  ptrecube  33539  poimirlem26  33565  poimirlem27  33566  heicant  33574  mbfresfi  33586  itg2addnc  33594  ftc1anc  33623  filbcmb  33665  sdclem2  33668  fdc  33671  fdc1  33672  rngoidmlem  33865  divrngidl  33957  pridlval  33962  smprngopr  33981  inecmo  34260  elcnvrefrels3  34421  ax12inda  34552  ax12v2-o  34553  isat3  34912  iscvlat2N  34929  psubspset  35348  ldilfset  35712  ldilset  35713  dilfsetN  35757  dilsetN  35758  cdlemefrs29bpre0  36001  cdlemefrs29clN  36004  cdlemefrs32fva  36005  cdlemn11pre  36816  dihord2pre  36831  lpolsetN  37088  aomclem8  37948  hbtlem5  38015  acsfn1p  38086  ifpbi1  38139  ifpbi12  38150  ifpbi13  38151  ntrneik2  38707  ntrneikb  38709  gneispacess2  38761  2sbc6g  38933  sbiota1  38952  uzwo4  39535  fsumiunss  40125  mullimc  40166  limcdm0  40168  mullimcf  40173  constlimc  40174  idlimc  40176  limsupre  40191  limcleqr  40194  addlimc  40198  0ellimcdiv  40199  limsupref  40235  limsupbnd1f  40236  limsupmnf  40271  limsupre2  40275  limsupmnfuzlem  40276  limsupre2mpt  40280  limsupre3  40283  limsupre3mpt  40284  limsupre3uzlem  40285  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvmptfprodlem  40477  wallispilem3  40602  fourierdlem48  40689  fourierdlem87  40728  sge0f1o  40917  sge0iunmptlemre  40950  sge0iunmpt  40953  vonioo  41217  vonicc  41220  bgoldbachlt  42026  tgoldbachlt  42029  bgoldbachltOLD  42032  tgoldbachltOLD  42035  sprsymrelfolem2  42068  ply1mulgsumlem1  42499  ply1mulgsumlem2  42500  elbigo2  42671  elbigo2r  42672  setrecseq  42757  setrec1lem1  42759  aacllem  42875
  Copyright terms: Public domain W3C validator