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

Theorem imbi1d 324
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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi1d  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 231 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 77 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 212 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 77 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 195 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  imbi12d  327  imbi1  330  imim21b  374  pm5.33  895  con3ALT  1002  con3OLD  1005  19.21t  2006  axc15  2153  ax12v2OLD  2191  drsb1  2226  ralcom2  2941  raleqf  2969  ralxpxfr2d  3152  alexeqg  3156  mo2icl  3205  sbc19.21g  3320  csbiebg  3372  ralss  3481  r19.37zv  3856  ssuni  4212  intmin4  4255  ssexg  4542  pocl  4767  vtoclr  4884  frsn  4910  fun11  5658  funimass4  5930  dff13  6177  f1mpt  6180  isopolem  6254  oprabid  6335  caovcan  6492  caoftrn  6585  ordunisuc2  6690  tfisi  6704  tfinds  6705  tfindsg  6706  tfindsg2  6707  dfom2  6713  findsg  6739  frxp  6925  dfsmo2  7084  qliftfun  7466  ecoptocl  7471  ecopovtrn  7484  dom2lem  7627  findcard  7828  findcard2  7829  findcard3  7832  fiint  7866  supmo  7984  eqsup  7988  suplub  7992  supmaxlemOLD  8000  supisoex  8008  infmo  8029  wemaplem1  8079  wemaplem2  8080  wemapsolem  8083  oemapvali  8207  cantnf  8216  wemapwe  8220  karden  8384  aceq1  8566  zorn2lem1  8944  axrepndlem2  9036  axregndlem2  9046  pwfseqlem4  9105  gruurn  9241  indpi  9350  nqereu  9372  prcdnq  9436  supexpr  9497  ltsosr  9536  supsrlem  9553  supsr  9554  axpre-lttrn  9608  axpre-sup  9611  prodgt0  10472  infm3  10590  prime  11039  raluz  11230  zsupss  11276  uzsupss  11279  xrsupsslem  11617  xrinfmsslem  11618  fz1sbc  11896  ssnn0fi  12235  fi1uzind  12691  brfi1indALT  12694  fi1uzindOLD  12697  brfi1indALTOLD  12700  wrdind  12887  wrd2ind  12888  relexprelg  13178  rtrclreclem3  13200  relexpindlem  13203  relexpind  13204  rtrclind  13205  rexanre  13486  rexico  13493  limsupgle  13612  rlim2lt  13638  rlim3  13639  ello12  13657  ello12r  13658  ello1d  13664  elo12  13668  elo12r  13669  rlimconst  13685  lo1resb  13705  o1resb  13707  rlimcn2  13731  addcn2  13734  mulcn2  13736  reccn2  13737  cn1lem  13738  o1rlimmul  13759  lo1le  13792  caucvgrlem  13813  caucvgrlemOLD  13814  divrcnv  13987  rpnnen2  14355  sqrt2irr  14378  exprmfct  14727  isprm5  14730  prmdvdsexpr  14748  prmpwdvds  14927  vdwmc2  15008  ramtlecl  15030  ramub  15049  rami  15051  ramcl  15066  firest  15409  mreexexd  15632  acsfn  15643  prslem  16254  ispos  16270  posi  16273  isposd  16279  lubeldm  16305  lubval  16308  glbeldm  16318  glbval  16321  joinval2lem  16332  meetval2lem  16346  pospropd  16458  odlem1  17259  odlem1OLD  17262  mndodcongi  17270  gexlem1  17306  gexlem1OLD  17308  sylow1lem3  17330  efgredlemb  17474  efgred  17476  frgpnabllem1  17587  isrrg  18589  mplsubglem  18735  mpllsslem  18736  ltbval  18772  opsrval  18775  xrsdsreclb  19092  islindf4  19473  mdetunilem1  19714  mdetunilem3  19716  mdetunilem4  19717  mdetunilem9  19722  chpscmat  19943  chfacffsupp  19957  chfacfscmulfsupp  19960  chfacfpmmulfsupp  19964  istopg  20002  isclo2  20181  neiptoptop  20224  neiptopnei  20225  lmbr  20351  ist0  20413  ist1-2  20440  t1sep2  20462  cmpfi  20500  2ndcdisj  20548  1stccn  20555  iskgen3  20641  ptpjopn  20704  hausdiag  20737  xkopt  20747  ist0-4  20821  isr0  20829  r0sep  20840  fbfinnfr  20934  fmfnfmlem2  21048  fmfnfmlem4  21050  fmfnfm  21051  cnflf  21095  cnfcf  21135  tmdgsum2  21189  tsmsgsum  21231  tsmsres  21236  tsmsf1o  21237  tsmsxplem1  21245  tsmsxp  21247  ustssel  21298  ustincl  21300  ustdiag  21301  ustinvel  21302  ustexhalf  21303  ust0  21312  ustuqtop4  21337  utopsnneiplem  21340  isucn2  21372  iducn  21376  metcnp  21634  metcnpi3  21639  txmetcnp  21640  metucn  21664  ngptgp  21722  nlmvscnlem1  21767  nrginvrcnlem  21771  nghmcn  21844  xrge0tsms  21930  xmetdcn2  21933  metdscn  21951  metdscnOLD  21966  addcnlem  21974  elcncf1di  22005  ipcnlem1  22294  caucfil  22331  metcld  22353  metcld2  22354  volcn  22643  itg2cnlem2  22799  ellimc2  22911  dveflem  23010  dvne0  23042  mdegleb  23092  mdegle0  23105  ply1divex  23166  fta1g  23197  dgrco  23308  plydivex  23329  fta1  23340  vieta1  23344  abelthlem8  23473  divlogrlim  23659  cxpcn3lem  23766  rlimcnp  23970  cxplim  23976  cxploglim  23982  ftalem1  24076  ftalem2  24077  dvdsmulf1o  24202  ppiublem1  24209  dchrinv  24268  lgseisenlem2  24357  2sqlem6  24376  2sqlem8  24379  2sqlem10  24381  dchrisum0  24437  istrkgc  24581  istrkgb  24582  axtgcgrid  24590  axtg5seg  24592  axtgpasch  24594  axtgeucl  24599  tgcgr4  24655  axlowdimlem15  25065  usgra2wlkspthlem1  25426  usgra2wlkspthlem2  25427  3v3e3cycl1  25451  constr3trllem2  25458  4cycl4v4e  25473  4cycl4dv4e  25475  eupatrl  25775  frgrawopreglem2  25852  usg2spot2nb  25872  friendshipgt3  25928  rngoidmlem  26232  isnvlem  26310  vacn  26411  nmcvcn  26412  smcnlem  26414  blocni  26527  norm3lemt  26886  isch2  26957  chlimi  26968  omlsii  27137  eigorth  27572  0cnop  27713  0cnfn  27714  idcnop  27715  lnconi  27767  stcltr1i  28008  elat2  28074  funcnv5mpt  28347  xrge0infss  28415  xrge0infssOLD  28416  resspos  28495  xrge0tsmsd  28622  qqhcn  28869  qqhucn  28870  esum2d  28988  eulerpartlemgvv  29282  sgn3da  29485  sgnnbi  29489  sgnpbi  29490  axtgupdim2OLD  29557  bnj1145  29874  bnj1171  29881  bnj1172  29882  erdszelem8  29993  mclsval  30273  mclsax  30279  mclsppslem  30293  ghomf1olem  30384  climuzcnv  30387  poseq  30562  frrlem4  30588  nocvxminlem  30650  ifscgr  30882  idinside  30922  brsegle  30946  trer  31043  filnetlem4  31108  bj-ssbequ  31306  bj-ssblem1  31307  bj-ssblem2  31308  bj-ssb1a  31309  bj-ssb1  31310  bj-ssbcom3lem  31327  bj-axc15v  31428  bj-19.21t  31498  wl-sbrimt  31948  fin2so  31996  ptrecube  32004  poimirlem26  32030  poimirlem27  32031  heicant  32039  mbfresfi  32051  itg2addnc  32060  ftc1anc  32089  filbcmb  32131  sdclem2  32135  fdc  32138  fdc1  32139  divrngidl  32325  pridlval  32330  smprngopr  32349  ax12inda  32583  ax12v2-o  32584  isat3  32944  iscvlat2N  32961  psubspset  33380  ldilfset  33744  ldilset  33745  dilfsetN  33789  dilsetN  33790  cdlemefrs29bpre0  34034  cdlemefrs29clN  34037  cdlemefrs32fva  34038  cdlemn11pre  34849  dihord2pre  34864  lpolsetN  35121  aomclem8  35990  hbtlem5  36058  acsfn1p  36136  ifpbi1  36192  ifpbi12  36203  ifpbi13  36204  isprm7  36730  2sbc6g  36836  sbiota1  36855  uzwo4  37451  fsumiunss  37750  mullimc  37793  limcdm0  37795  mullimcf  37800  constlimc  37801  idlimc  37803  limsupre  37818  limsupreOLD  37819  limcleqr  37822  addlimc  37826  0ellimcdiv  37827  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvmptfprodlem  37916  wallispilem3  38041  fourierdlem48  38130  fourierdlem87  38169  sge0f1o  38338  sge0iunmptlemre  38371  sge0iunmpt  38374  bgoldbachlt  39051  tgoldbachlt  39054  usgr2wlkneq  39948  usgra2pthspth  40173  usgra2pthlem1  40175  ply1mulgsumlem1  40686  ply1mulgsumlem2  40687  elbigo2  40871  elbigo2r  40872  aacllem  41046
  Copyright terms: Public domain W3C validator