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

Theorem imbi1d 309
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 215 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 71 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 199 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 71 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 184 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  imbi12d  312  imbi1  314  imim21b  357  pm5.33  849  con3th  925  ax12bOLD  1697  19.21t  1803  ax11v2  2031  drsb1  2057  ax11vALT  2132  ax11inda  2236  ax11v2-o  2237  ralcom2  2817  raleqf  2845  alexeq  3010  mo2icl  3058  sbc19.21g  3170  csbiebg  3235  ralss  3354  r19.37zv  3669  ssuni  3981  intmin4  4023  ssexg  4292  pocl  4453  ordunisuc2  4766  tfisi  4780  tfinds  4781  tfindsg  4782  tfindsg2  4783  dfom2  4789  findsg  4814  vtoclr  4864  frsn  4890  fun11  5458  funimass4  5718  dff13  5945  f1mpt  5948  isopolem  6006  oprabid  6046  caovcan  6192  caoftrn  6280  frxp  6394  dfsmo2  6547  qliftfun  6927  ecoptocl  6932  ecopovtrn  6945  dom2lem  7085  findcard  7285  findcard2  7286  findcard3  7288  fiint  7321  supmo  7392  eqsup  7396  suplub  7400  supmaxlem  7404  supisoex  7411  wemaplem1  7450  wemaplem2  7451  wemapso2lem  7454  oemapvali  7575  cantnf  7584  wemapwe  7589  karden  7754  aceq1  7933  zorn2lem1  8311  axrepndlem2  8403  axregndlem2  8413  pwfseqlem4  8472  gruurn  8608  indpi  8719  nqereu  8741  prcdnq  8805  supexpr  8866  ltsosr  8904  supsrlem  8921  supsr  8922  axpre-lttrn  8976  axpre-sup  8979  prodgt0  9789  infm3  9901  prime  10284  raluz  10459  zsupss  10499  uzsupss  10502  xrsupsslem  10819  xrinfmsslem  10820  fz1sbc  11056  brfi1uzind  11644  wrdind  11720  rexanre  12079  rexico  12086  limsupgle  12200  rlim2lt  12220  rlim3  12221  ello12  12239  ello12r  12240  ello1d  12246  elo12  12250  elo12r  12251  rlimconst  12267  lo1resb  12287  o1resb  12289  rlimcn2  12313  addcn2  12316  mulcn2  12318  reccn2  12319  cn1lem  12320  o1rlimmul  12341  lo1le  12374  caucvgrlem  12395  divrcnv  12561  rpnnen2  12754  sqr2irr  12777  exprmfct  13039  isprm5  13041  prmdvdsexpr  13045  prmpwdvds  13201  vdwmc2  13276  ramtlecl  13297  ramub  13310  rami  13312  ramcl  13326  firest  13589  mreexexd  13802  acsfn  13813  prslem  14317  ispos  14333  posi  14336  isposd  14341  lubval  14365  glbval  14370  joinval2  14375  meetval2  14382  pospropd  14490  spwval2  14585  spwpr2  14589  odlem1  15102  mndodcongi  15110  gexlem1  15142  sylow1lem3  15163  efgredlemb  15307  efgred  15309  frgpnabllem1  15413  isrrg  16277  mplsubglem  16427  mpllsslem  16428  ltbval  16461  opsrval  16464  xrsdsreclb  16670  istopg  16893  isclo2  17077  neiptoptop  17120  neiptopnei  17121  lmbr  17246  ist0  17308  ist1-2  17335  t1sep2  17357  cmpfi  17395  2ndcdisj  17442  1stccn  17449  iskgen3  17504  ptpjopn  17567  hausdiag  17600  xkopt  17610  ist0-4  17684  isr0  17692  r0sep  17703  fbfinnfr  17796  fmfnfmlem2  17910  fmfnfmlem4  17912  fmfnfm  17913  cnflf  17957  cnfcf  17997  tmdgsum2  18049  tsmsgsum  18091  tsmsres  18096  tsmsf1o  18097  tsmsxplem1  18105  tsmsxp  18107  ustssel  18158  ustincl  18160  ustdiag  18161  ustinvel  18162  ustexhalf  18163  ust0  18172  ustuqtop4  18197  utopsnneiplem  18200  isucn2  18232  iducn  18236  metcnp  18463  metcnpi3  18468  txmetcnp  18469  metucn  18492  ngptgp  18550  nlmvscnlem1  18595  nrginvrcnlem  18599  nghmcn  18652  xrge0tsms  18738  xmetdcn2  18741  metdscn  18759  addcnlem  18767  elcncf1di  18798  ipcnlem1  19072  caucfil  19109  metcld  19131  metcld2  19132  volcn  19367  itg2cnlem2  19523  ellimc2  19633  dveflem  19732  dvne0  19764  mdegleb  19856  mdegle0  19869  ply1divex  19928  fta1g  19959  dgrco  20062  plydivex  20083  fta1  20094  vieta1  20098  abelthlem8  20224  divlogrlim  20395  cxpcn3lem  20500  rlimcnp  20673  cxplim  20679  cxploglim  20685  ftalem1  20724  ftalem2  20725  dvdsmulf1o  20848  ppiublem1  20855  dchrinv  20914  lgseisenlem2  21003  2sqlem6  21022  2sqlem8  21025  2sqlem10  21027  dchrisum0  21083  3v3e3cycl1  21481  constr3trllem2  21488  4cycl4v4e  21503  4cycl4dv4e  21505  eupatrl  21540  rngoidmlem  21861  isnvlem  21939  vacn  22040  nmcvcn  22041  smcnlem  22043  blocni  22156  norm3lemt  22504  isch2  22576  chlimi  22587  omlsii  22755  eigorth  23191  0cnop  23332  0cnfn  23333  idcnop  23334  lnconi  23386  stcltr1i  23627  elat2  23693  funcnv5mpt  23927  resspos  24028  xrge0tsmsd  24054  qqhcn  24176  qqhucn  24177  erdszelem8  24665  ghomf1olem  24886  climuzcnv  24889  relexpindlem  24920  relexpind  24921  rtrclreclem.trans  24927  rtrclind  24930  poseq  25279  frrlem4  25310  nocvxminlem  25370  elfuns  25480  axlowdimlem15  25611  ifscgr  25694  idinside  25734  brsegle  25758  trer  26012  filnetlem4  26103  filbcmb  26135  sdclem2  26139  fdc  26142  fdc1  26143  divrngidl  26331  pridlval  26336  smprngopr  26355  ralxpxfr2d  26434  aomclem8  26830  islindf4  26979  hbtlem5  27003  acsfn1p  27178  2sbc6g  27286  sbiota1  27305  wallispilem3  27486  frgrawopreglem2  27799  bnj1145  28702  bnj1171  28709  bnj1172  28710  drsb1NEW7  28846  ax11v2NEW7  28868  isat3  29424  iscvlat2N  29441  psubspset  29860  ldilfset  30224  ldilset  30225  dilfsetN  30268  dilsetN  30269  cdlemefrs29bpre0  30512  cdlemefrs29clN  30515  cdlemefrs32fva  30516  cdlemn11pre  31327  dihord2pre  31342  lpolsetN  31599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator