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

Theorem imbi1d 315
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 223 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 75 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 207 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 75 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 191 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  imbi12d  318  imbi1  321  imim21b  365  pm5.33  879  con3th  959  ax12vOLD  1880  19.21t  1932  ax12v2  2109  drsb1  2142  ralcom2  2971  raleqf  2999  ralxpxfr2d  3173  alexeqg  3177  alexeq  3178  mo2icl  3227  sbc19.21g  3341  csbiebg  3395  ralss  3504  r19.37zv  3868  ssuni  4212  intmin4  4256  ssexg  4539  pocl  4750  vtoclr  4867  frsn  4893  fun11  5633  funimass4  5899  dff13  6146  f1mpt  6149  isopolem  6223  oprabid  6304  caovcan  6459  caoftrn  6556  ordunisuc2  6661  tfisi  6675  tfinds  6676  tfindsg  6677  tfindsg2  6678  dfom2  6684  findsg  6710  frxp  6893  dfsmo2  7050  qliftfun  7432  ecoptocl  7437  ecopovtrn  7450  dom2lem  7592  findcard  7792  findcard2  7793  findcard3  7796  fiint  7830  supmo  7944  eqsup  7948  suplub  7952  supmaxlemOLD  7957  supisoex  7965  wemaplem1  8004  wemaplem2  8005  wemapsolem  8008  oemapvali  8134  cantnf  8143  cantnfOLD  8165  wemapwe  8170  wemapweOLD  8171  karden  8344  aceq1  8529  zorn2lem1  8907  axrepndlem2  8999  axregndlem2  9009  pwfseqlem4  9069  gruurn  9205  indpi  9314  nqereu  9336  prcdnq  9400  supexpr  9461  ltsosr  9500  supsrlem  9517  supsr  9518  axpre-lttrn  9572  axpre-sup  9575  prodgt0  10427  infm3  10541  prime  10983  raluz  11174  zsupss  11215  uzsupss  11218  xrsupsslem  11550  xrinfmsslem  11551  fz1sbc  11807  ssnn0fi  12133  brfi1uzind  12579  wrdind  12756  wrd2ind  12757  relexprelg  13018  rtrclreclem3  13040  relexpindlem  13043  relexpind  13044  rtrclind  13045  rexanre  13326  rexico  13333  limsupgle  13447  rlim2lt  13467  rlim3  13468  ello12  13486  ello12r  13487  ello1d  13493  elo12  13497  elo12r  13498  rlimconst  13514  lo1resb  13534  o1resb  13536  rlimcn2  13560  addcn2  13563  mulcn2  13565  reccn2  13566  cn1lem  13567  o1rlimmul  13588  lo1le  13621  caucvgrlem  13642  divrcnv  13813  rpnnen2  14166  sqrt2irr  14189  exprmfct  14458  isprm5  14460  prmdvdsexpr  14464  prmpwdvds  14629  vdwmc2  14704  ramtlecl  14725  ramub  14738  rami  14740  ramcl  14754  firest  15045  mreexexd  15260  acsfn  15271  prslem  15882  ispos  15898  posi  15901  isposd  15907  lubeldm  15933  lubval  15936  glbeldm  15946  glbval  15949  joinval2lem  15960  meetval2lem  15974  pospropd  16086  odlem1  16881  mndodcongi  16889  gexlem1  16921  sylow1lem3  16942  efgredlemb  17086  efgred  17088  frgpnabllem1  17199  isrrg  18254  mplsubglem  18411  mpllsslem  18412  mplsubglemOLD  18413  mpllsslemOLD  18414  ltbval  18454  opsrval  18457  xrsdsreclb  18783  islindf4  19163  mdetunilem1  19404  mdetunilem3  19406  mdetunilem4  19407  mdetunilem9  19412  chpscmat  19633  chfacffsupp  19647  chfacfscmulfsupp  19650  chfacfpmmulfsupp  19654  istopg  19694  isclo2  19880  neiptoptop  19923  neiptopnei  19924  lmbr  20050  ist0  20112  ist1-2  20139  t1sep2  20161  cmpfi  20199  2ndcdisj  20247  1stccn  20254  iskgen3  20340  ptpjopn  20403  hausdiag  20436  xkopt  20446  ist0-4  20520  isr0  20528  r0sep  20539  fbfinnfr  20632  fmfnfmlem2  20746  fmfnfmlem4  20748  fmfnfm  20749  cnflf  20793  cnfcf  20833  tmdgsum2  20885  tsmsgsum  20927  tsmsgsumOLD  20930  tsmsresOLD  20935  tsmsres  20936  tsmsf1o  20937  tsmsxplem1  20945  tsmsxp  20947  ustssel  20998  ustincl  21000  ustdiag  21001  ustinvel  21002  ustexhalf  21003  ust0  21012  ustuqtop4  21037  utopsnneiplem  21040  isucn2  21072  iducn  21076  metcnp  21334  metcnpi3  21339  txmetcnp  21340  metucnOLD  21381  metucn  21382  ngptgp  21440  nlmvscnlem1  21485  nrginvrcnlem  21489  nghmcn  21542  xrge0tsms  21629  xmetdcn2  21632  metdscn  21650  addcnlem  21658  elcncf1di  21689  ipcnlem1  21975  caucfil  22012  metcld  22034  metcld2  22035  volcn  22305  itg2cnlem2  22459  ellimc2  22571  dveflem  22670  dvne0  22702  mdegleb  22754  mdegle0  22767  ply1divex  22827  fta1g  22858  dgrco  22962  plydivex  22983  fta1  22994  vieta1  22998  abelthlem8  23124  divlogrlim  23308  cxpcn3lem  23415  rlimcnp  23619  cxplim  23625  cxploglim  23631  ftalem1  23725  ftalem2  23726  dvdsmulf1o  23849  ppiublem1  23856  dchrinv  23915  lgseisenlem2  24004  2sqlem6  24023  2sqlem8  24026  2sqlem10  24028  dchrisum0  24084  istrkgc  24228  istrkgb  24229  axtgcgrid  24237  axtg5seg  24239  axtgpasch  24241  axtgeucl  24246  axlowdimlem15  24663  usgra2wlkspthlem1  25023  usgra2wlkspthlem2  25024  3v3e3cycl1  25048  constr3trllem2  25055  4cycl4v4e  25070  4cycl4dv4e  25072  eupatrl  25372  frgrawopreglem2  25449  usg2spot2nb  25469  friendshipgt3  25525  rngoidmlem  25825  isnvlem  25903  vacn  26004  nmcvcn  26005  smcnlem  26007  blocni  26120  norm3lemt  26469  isch2  26541  chlimi  26552  omlsii  26721  eigorth  27156  0cnop  27297  0cnfn  27298  idcnop  27299  lnconi  27351  stcltr1i  27592  elat2  27658  funcnv5mpt  27940  xrge0infss  28008  resspos  28085  xrge0tsmsd  28214  qqhcn  28410  qqhucn  28411  esum2d  28526  eulerpartlemgvv  28807  sgn3da  28972  sgnnbi  28976  sgnpbi  28977  axtgupdim2OLD  29045  bnj1145  29363  bnj1171  29370  bnj1172  29371  erdszelem8  29482  mclsval  29762  mclsax  29768  mclsppslem  29782  ghomf1olem  29873  climuzcnv  29876  poseq  30051  frrlem4  30077  nocvxminlem  30137  ifscgr  30369  idinside  30409  brsegle  30433  trer  30531  filnetlem4  30596  bj-con3thALT  30713  bj-axc15v  30881  bj-19.21t  30954  wl-sbrimt  31350  fin2so  31392  heicant  31401  mbfresfi  31413  itg2addnc  31422  ftc1anc  31451  filbcmb  31493  sdclem2  31497  fdc  31500  fdc1  31501  divrngidl  31687  pridlval  31692  smprngopr  31711  ax12inda  31951  ax12v2-o  31952  isat3  32305  iscvlat2N  32322  psubspset  32741  ldilfset  33105  ldilset  33106  dilfsetN  33150  dilsetN  33151  cdlemefrs29bpre0  33395  cdlemefrs29clN  33398  cdlemefrs32fva  33399  cdlemn11pre  34210  dihord2pre  34225  lpolsetN  34482  aomclem8  35349  hbtlem5  35421  acsfn1p  35492  ifpbi1  35548  ifpbi12  35559  ifpbi13  35560  isprm7  36020  2sbc6g  36150  sbiota1  36169  mullimc  36971  limcdm0  36973  mullimcf  36978  constlimc  36979  idlimc  36981  limsupre  36996  limcleqr  36999  addlimc  37003  0ellimcdiv  37004  ioodvbdlimc1lem2  37078  ioodvbdlimc2lem  37080  dvmptfprodlem  37090  wallispilem3  37198  fourierdlem48  37286  fourierdlem87  37325  usgra2pthspth  37961  usgra2pthlem1  37963  ply1mulgsumlem1  38478  ply1mulgsumlem2  38479  elbigo2  38664  elbigo2r  38665  aacllem  38841
  Copyright terms: Public domain W3C validator