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

Theorem imbi1d 317
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  320  imbi1  323  imim21b  367  pm5.33  876  con3th  956  ax12vOLD  1805  19.21t  1852  ax12v2  2056  drsb1  2091  ax12inda  2271  ax12v2-o  2272  ralcom2  3026  raleqf  3054  ralxpxfr2d  3228  alexeqg  3232  alexeq  3233  mo2icl  3282  sbc19.21g  3404  csbiebg  3458  ralss  3566  r19.37zv  3924  ssuni  4267  intmin4  4311  ssexg  4593  pocl  4807  vtoclr  5044  frsn  5070  fun11  5653  funimass4  5918  dff13  6154  f1mpt  6157  isopolem  6229  oprabid  6308  caovcan  6463  caoftrn  6559  ordunisuc2  6663  tfisi  6677  tfinds  6678  tfindsg  6679  tfindsg2  6680  dfom2  6686  findsg  6711  frxp  6893  dfsmo2  7018  qliftfun  7396  ecoptocl  7401  ecopovtrn  7414  dom2lem  7555  findcard  7759  findcard2  7760  findcard3  7763  fiint  7797  supmo  7912  eqsup  7916  suplub  7920  supmaxlem  7924  supisoex  7932  wemaplem1  7971  wemaplem2  7972  wemapsolem  7975  oemapvali  8103  cantnf  8112  cantnfOLD  8134  wemapwe  8139  wemapweOLD  8140  karden  8313  aceq1  8498  zorn2lem1  8876  axrepndlem2  8968  axregndlem2  8980  pwfseqlem4  9040  gruurn  9176  indpi  9285  nqereu  9307  prcdnq  9371  supexpr  9432  ltsosr  9471  supsrlem  9488  supsr  9489  axpre-lttrn  9543  axpre-sup  9546  prodgt0  10387  infm3  10502  prime  10941  raluz  11129  zsupss  11171  uzsupss  11174  xrsupsslem  11498  xrinfmsslem  11499  fz1sbc  11754  ssnn0fi  12062  brfi1uzind  12498  wrdind  12665  wrd2ind  12666  rexanre  13142  rexico  13149  limsupgle  13263  rlim2lt  13283  rlim3  13284  ello12  13302  ello12r  13303  ello1d  13309  elo12  13313  elo12r  13314  rlimconst  13330  lo1resb  13350  o1resb  13352  rlimcn2  13376  addcn2  13379  mulcn2  13381  reccn2  13382  cn1lem  13383  o1rlimmul  13404  lo1le  13437  caucvgrlem  13458  divrcnv  13627  rpnnen2  13820  sqrt2irr  13843  exprmfct  14110  isprm5  14112  prmdvdsexpr  14116  prmpwdvds  14281  vdwmc2  14356  ramtlecl  14377  ramub  14390  rami  14392  ramcl  14406  firest  14688  mreexexd  14903  acsfn  14914  prslem  15418  ispos  15434  posi  15437  isposd  15442  lubeldm  15468  lubval  15471  glbeldm  15481  glbval  15484  joinval2lem  15495  meetval2lem  15509  pospropd  15621  odlem1  16365  mndodcongi  16373  gexlem1  16405  sylow1lem3  16426  efgredlemb  16570  efgred  16572  frgpnabllem1  16680  isrrg  17735  mplsubglem  17892  mpllsslem  17893  mplsubglemOLD  17894  mpllsslemOLD  17895  ltbval  17935  opsrval  17938  xrsdsreclb  18261  islindf4  18668  mdetunilem1  18909  mdetunilem3  18911  mdetunilem4  18912  mdetunilem9  18917  chpscmat  19138  chfacffsupp  19152  chfacfscmulfsupp  19155  chfacfpmmulfsupp  19159  istopg  19199  isclo2  19383  neiptoptop  19426  neiptopnei  19427  lmbr  19553  ist0  19615  ist1-2  19642  t1sep2  19664  cmpfi  19702  2ndcdisj  19751  1stccn  19758  iskgen3  19813  ptpjopn  19876  hausdiag  19909  xkopt  19919  ist0-4  19993  isr0  20001  r0sep  20012  fbfinnfr  20105  fmfnfmlem2  20219  fmfnfmlem4  20221  fmfnfm  20222  cnflf  20266  cnfcf  20306  tmdgsum2  20358  tsmsgsum  20400  tsmsgsumOLD  20403  tsmsresOLD  20408  tsmsres  20409  tsmsf1o  20410  tsmsxplem1  20418  tsmsxp  20420  ustssel  20471  ustincl  20473  ustdiag  20474  ustinvel  20475  ustexhalf  20476  ust0  20485  ustuqtop4  20510  utopsnneiplem  20513  isucn2  20545  iducn  20549  metcnp  20807  metcnpi3  20812  txmetcnp  20813  metucnOLD  20854  metucn  20855  ngptgp  20913  nlmvscnlem1  20958  nrginvrcnlem  20962  nghmcn  21015  xrge0tsms  21102  xmetdcn2  21105  metdscn  21123  addcnlem  21131  elcncf1di  21162  ipcnlem1  21448  caucfil  21485  metcld  21507  metcld2  21508  volcn  21778  itg2cnlem2  21932  ellimc2  22044  dveflem  22143  dvne0  22175  mdegleb  22227  mdegle0  22240  ply1divex  22300  fta1g  22331  dgrco  22434  plydivex  22455  fta1  22466  vieta1  22470  abelthlem8  22596  divlogrlim  22772  cxpcn3lem  22877  rlimcnp  23051  cxplim  23057  cxploglim  23063  ftalem1  23102  ftalem2  23103  dvdsmulf1o  23226  ppiublem1  23233  dchrinv  23292  lgseisenlem2  23381  2sqlem6  23400  2sqlem8  23403  2sqlem10  23405  dchrisum0  23461  istrkgc  23607  istrkgb  23608  axtgcgrid  23616  axtg5seg  23618  axtgpasch  23620  axtgupdim2  23625  axtgeucl  23626  axlowdimlem15  23963  usgra2wlkspthlem1  24323  usgra2wlkspthlem2  24324  3v3e3cycl1  24348  constr3trllem2  24355  4cycl4v4e  24370  4cycl4dv4e  24372  eupatrl  24672  frgrawopreglem2  24750  usg2spot2nb  24770  friendshipgt3  24826  rngoidmlem  25129  isnvlem  25207  vacn  25308  nmcvcn  25309  smcnlem  25311  blocni  25424  norm3lemt  25773  isch2  25845  chlimi  25856  omlsii  26025  eigorth  26461  0cnop  26602  0cnfn  26603  idcnop  26604  lnconi  26656  stcltr1i  26897  elat2  26963  funcnv5mpt  27211  xrge0infss  27276  resspos  27337  xrge0tsmsd  27466  rngurd  27469  qqhcn  27636  qqhucn  27637  eulerpartlemgvv  27983  sgn3da  28148  sgnnbi  28152  sgnpbi  28153  erdszelem8  28310  ghomf1olem  28537  climuzcnv  28540  relexpindlem  28565  relexpind  28566  rtrclreclem.trans  28572  rtrclind  28575  poseq  28938  frrlem4  28995  nocvxminlem  29055  ifscgr  29299  idinside  29339  brsegle  29363  wl-sbrimt  29603  fin2so  29645  heicant  29654  mbfresfi  29666  itg2addnc  29674  ftc1anc  29703  trer  29739  filnetlem4  29830  filbcmb  29862  sdclem2  29866  fdc  29869  fdc1  29870  divrngidl  30056  pridlval  30061  smprngopr  30080  aomclem8  30639  hbtlem5  30709  acsfn1p  30781  isprm7  30823  2sbc6g  30928  sbiota1  30947  mullimc  31186  limcdm0  31188  mullimcf  31193  constlimc  31194  idlimc  31196  limsupre  31211  limcleqr  31214  addlimc  31218  0ellimcdiv  31219  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  wallispilem3  31395  fourierdlem48  31483  fourierdlem87  31522  usgra2pthspth  31846  usgra2pthlem1  31848  ply1mulgsumlem1  32085  ply1mulgsumlem2  32086  bnj1145  33146  bnj1171  33153  bnj1172  33154  bj-con3ALT  33260  bj-axc15v  33429  bj-19.21t  33502  isat3  34122  iscvlat2N  34139  psubspset  34558  ldilfset  34922  ldilset  34923  dilfsetN  34966  dilsetN  34967  cdlemefrs29bpre0  35210  cdlemefrs29clN  35213  cdlemefrs32fva  35214  cdlemn11pre  36025  dihord2pre  36040  lpolsetN  36297
  Copyright terms: Public domain W3C validator