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

Theorem imbi1d 319
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 227 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 78 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 211 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 78 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 194 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  imbi12d  322  imbi1  325  imim21b  369  pm5.33  888  con3th  968  19.21t  1985  ax12v2  2174  drsb1  2205  ralcom2  2954  raleqf  2982  ralxpxfr2d  3163  alexeqg  3167  mo2icl  3216  sbc19.21g  3331  csbiebg  3385  ralss  3494  r19.37zv  3864  ssuni  4219  intmin4  4263  ssexg  4548  pocl  4761  vtoclr  4878  frsn  4904  fun11  5646  funimass4  5914  dff13  6157  f1mpt  6160  isopolem  6234  oprabid  6315  caovcan  6470  caoftrn  6563  ordunisuc2  6668  tfisi  6682  tfinds  6683  tfindsg  6684  tfindsg2  6685  dfom2  6691  findsg  6717  frxp  6903  dfsmo2  7063  qliftfun  7445  ecoptocl  7450  ecopovtrn  7463  dom2lem  7606  findcard  7807  findcard2  7808  findcard3  7811  fiint  7845  supmo  7963  eqsup  7967  suplub  7971  supmaxlemOLD  7979  supisoex  7987  infmo  8008  wemaplem1  8058  wemaplem2  8059  wemapsolem  8062  oemapvali  8186  cantnf  8195  wemapwe  8199  karden  8363  aceq1  8545  zorn2lem1  8923  axrepndlem2  9015  axregndlem2  9025  pwfseqlem4  9084  gruurn  9220  indpi  9329  nqereu  9351  prcdnq  9415  supexpr  9476  ltsosr  9515  supsrlem  9532  supsr  9533  axpre-lttrn  9587  axpre-sup  9590  prodgt0  10447  infm3  10565  prime  11013  raluz  11204  zsupss  11250  uzsupss  11253  xrsupsslem  11589  xrinfmsslem  11590  fz1sbc  11867  ssnn0fi  12194  fi1uzind  12647  brfi1indALT  12650  wrdind  12828  wrd2ind  12829  relexprelg  13094  rtrclreclem3  13116  relexpindlem  13119  relexpind  13120  rtrclind  13121  rexanre  13402  rexico  13409  limsupgle  13528  rlim2lt  13554  rlim3  13555  ello12  13573  ello12r  13574  ello1d  13580  elo12  13584  elo12r  13585  rlimconst  13601  lo1resb  13621  o1resb  13623  rlimcn2  13647  addcn2  13650  mulcn2  13652  reccn2  13653  cn1lem  13654  o1rlimmul  13675  lo1le  13708  caucvgrlem  13729  caucvgrlemOLD  13730  divrcnv  13903  rpnnen2  14271  sqrt2irr  14294  exprmfct  14641  isprm5  14644  prmdvdsexpr  14662  prmpwdvds  14841  vdwmc2  14922  ramtlecl  14944  ramub  14963  rami  14965  ramcl  14980  firest  15324  mreexexd  15547  acsfn  15558  prslem  16169  ispos  16185  posi  16188  isposd  16194  lubeldm  16220  lubval  16223  glbeldm  16233  glbval  16236  joinval2lem  16247  meetval2lem  16261  pospropd  16373  odlem1  17174  odlem1OLD  17177  mndodcongi  17185  gexlem1  17221  gexlem1OLD  17223  sylow1lem3  17245  efgredlemb  17389  efgred  17391  frgpnabllem1  17502  isrrg  18505  mplsubglem  18651  mpllsslem  18652  ltbval  18688  opsrval  18691  xrsdsreclb  19008  islindf4  19389  mdetunilem1  19630  mdetunilem3  19632  mdetunilem4  19633  mdetunilem9  19638  chpscmat  19859  chfacffsupp  19873  chfacfscmulfsupp  19876  chfacfpmmulfsupp  19880  istopg  19918  isclo2  20097  neiptoptop  20140  neiptopnei  20141  lmbr  20267  ist0  20329  ist1-2  20356  t1sep2  20378  cmpfi  20416  2ndcdisj  20464  1stccn  20471  iskgen3  20557  ptpjopn  20620  hausdiag  20653  xkopt  20663  ist0-4  20737  isr0  20745  r0sep  20756  fbfinnfr  20849  fmfnfmlem2  20963  fmfnfmlem4  20965  fmfnfm  20966  cnflf  21010  cnfcf  21050  tmdgsum2  21104  tsmsgsum  21146  tsmsres  21151  tsmsf1o  21152  tsmsxplem1  21160  tsmsxp  21162  ustssel  21213  ustincl  21215  ustdiag  21216  ustinvel  21217  ustexhalf  21218  ust0  21227  ustuqtop4  21252  utopsnneiplem  21255  isucn2  21287  iducn  21291  metcnp  21549  metcnpi3  21554  txmetcnp  21555  metucn  21579  ngptgp  21637  nlmvscnlem1  21682  nrginvrcnlem  21686  nghmcn  21759  xrge0tsms  21845  xmetdcn2  21848  metdscn  21866  metdscnOLD  21881  addcnlem  21889  elcncf1di  21920  ipcnlem1  22209  caucfil  22246  metcld  22268  metcld2  22269  volcn  22557  itg2cnlem2  22713  ellimc2  22825  dveflem  22924  dvne0  22956  mdegleb  23006  mdegle0  23019  ply1divex  23080  fta1g  23111  dgrco  23222  plydivex  23243  fta1  23254  vieta1  23258  abelthlem8  23387  divlogrlim  23573  cxpcn3lem  23680  rlimcnp  23884  cxplim  23890  cxploglim  23896  ftalem1  23990  ftalem2  23991  dvdsmulf1o  24116  ppiublem1  24123  dchrinv  24182  lgseisenlem2  24271  2sqlem6  24290  2sqlem8  24293  2sqlem10  24295  dchrisum0  24351  istrkgc  24495  istrkgb  24496  axtgcgrid  24504  axtg5seg  24506  axtgpasch  24508  axtgeucl  24513  tgcgr4  24569  axlowdimlem15  24979  usgra2wlkspthlem1  25340  usgra2wlkspthlem2  25341  3v3e3cycl1  25365  constr3trllem2  25372  4cycl4v4e  25387  4cycl4dv4e  25389  eupatrl  25689  frgrawopreglem2  25766  usg2spot2nb  25786  friendshipgt3  25842  rngoidmlem  26144  isnvlem  26222  vacn  26323  nmcvcn  26324  smcnlem  26326  blocni  26439  norm3lemt  26798  isch2  26869  chlimi  26880  omlsii  27049  eigorth  27484  0cnop  27625  0cnfn  27626  idcnop  27627  lnconi  27679  stcltr1i  27920  elat2  27986  funcnv5mpt  28265  xrge0infss  28333  xrge0infssOLD  28334  resspos  28413  xrge0tsmsd  28541  qqhcn  28788  qqhucn  28789  esum2d  28907  eulerpartlemgvv  29202  sgn3da  29405  sgnnbi  29409  sgnpbi  29410  axtgupdim2OLD  29478  bnj1145  29795  bnj1171  29802  bnj1172  29803  erdszelem8  29914  mclsval  30194  mclsax  30200  mclsppslem  30214  ghomf1olem  30305  climuzcnv  30308  poseq  30484  frrlem4  30510  nocvxminlem  30572  ifscgr  30804  idinside  30844  brsegle  30868  trer  30965  filnetlem4  31030  bj-con3thALT  31148  bj-ssbequ  31235  bj-ssblem1  31236  bj-ssblem2  31237  bj-ssb1a  31238  bj-ssb1  31239  bj-ssbcom3lem  31256  bj-axc15v  31355  bj-19.21t  31425  wl-sbrimt  31871  wl-ax12v3  31905  fin2so  31925  ptrecube  31933  poimirlem26  31959  poimirlem27  31960  heicant  31968  mbfresfi  31980  itg2addnc  31989  ftc1anc  32018  filbcmb  32060  sdclem2  32064  fdc  32067  fdc1  32068  divrngidl  32254  pridlval  32259  smprngopr  32278  ax12inda  32513  ax12v2-o  32514  isat3  32867  iscvlat2N  32884  psubspset  33303  ldilfset  33667  ldilset  33668  dilfsetN  33712  dilsetN  33713  cdlemefrs29bpre0  33957  cdlemefrs29clN  33960  cdlemefrs32fva  33961  cdlemn11pre  34772  dihord2pre  34787  lpolsetN  35044  aomclem8  35913  hbtlem5  35981  acsfn1p  36059  ifpbi1  36115  ifpbi12  36126  ifpbi13  36127  isprm7  36654  2sbc6g  36760  sbiota1  36779  uzwo4  37386  fsumiunss  37648  mullimc  37690  limcdm0  37692  mullimcf  37697  constlimc  37698  idlimc  37700  limsupre  37715  limsupreOLD  37716  limcleqr  37719  addlimc  37723  0ellimcdiv  37724  ioodvbdlimc1lem2  37798  ioodvbdlimc1lem2OLD  37800  ioodvbdlimc2lem  37802  ioodvbdlimc2lemOLD  37803  dvmptfprodlem  37813  wallispilem3  37923  fourierdlem48  38012  fourierdlem87  38051  sge0f1o  38218  sge0iunmptlemre  38251  sge0iunmpt  38254  bgoldbachlt  38900  tgoldbachlt  38903  usgra2pthspth  39652  usgra2pthlem1  39654  ply1mulgsumlem1  40165  ply1mulgsumlem2  40166  elbigo2  40350  elbigo2r  40351  aacllem  40527
  Copyright terms: Public domain W3C validator