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

Theorem imbi1d 308
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 214 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 69 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 198 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 69 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 183 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12d  311  imbi1  313  imim21b  356  pm5.33  848  con3th  924  ax12bOLD  1656  ax11v2  1932  drsb1  1962  ax11inda  2139  ax11v2-o  2140  ralcom2  2704  raleqf  2732  alexeq  2897  mo2icl  2944  sbc19.21g  3055  csbiebg  3120  ralss  3239  r19.37zv  3550  ssuni  3849  intmin4  3891  ssexg  4160  pocl  4321  ordunisuc2  4635  tfisi  4649  tfinds  4650  tfindsg  4651  tfindsg2  4652  dfom2  4658  findsg  4683  vtoclr  4733  frsn  4760  fun11  5315  funimass4  5573  dff13  5783  f1mpt  5785  isopolem  5842  oprabid  5882  caovcan  6024  caoftrn  6112  frxp  6225  dfsmo2  6364  qliftfun  6743  ecoptocl  6748  ecopovtrn  6761  dom2lem  6901  findcard  7097  findcard2  7098  findcard3  7100  fiint  7133  supmo  7203  eqsup  7207  suplub  7211  supmaxlem  7215  supisoex  7222  wemaplem1  7261  wemaplem2  7262  wemapso2lem  7265  oemapvali  7386  cantnf  7395  wemapwe  7400  karden  7565  aceq1  7744  zorn2lem1  8123  axrepndlem2  8215  axregndlem2  8225  pwfseqlem4  8284  gruurn  8420  indpi  8531  nqereu  8553  prcdnq  8617  supexpr  8678  ltsosr  8716  supsrlem  8733  supsr  8734  axpre-lttrn  8788  axpre-sup  8791  prodgt0  9601  lbinfm  9707  infm3  9713  prime  10092  raluz  10267  zsupss  10307  uzsupss  10310  xrsupsslem  10625  xrinfmsslem  10626  fz1sbc  10859  wrdind  11477  rexanre  11830  rexico  11837  limsupgle  11951  rlim2lt  11971  rlim3  11972  ello12  11990  ello12r  11991  ello1d  11997  elo12  12001  elo12r  12002  rlimconst  12018  lo1resb  12038  o1resb  12040  rlimcn2  12064  addcn2  12067  mulcn2  12069  reccn2  12070  cn1lem  12071  o1rlimmul  12092  lo1le  12125  caucvgrlem  12145  divrcnv  12311  rpnnen2  12504  sqr2irr  12527  exprmfct  12789  isprm5  12791  prmdvdsexpr  12795  prmpwdvds  12951  vdwmc2  13026  ramtlecl  13047  ramub  13060  rami  13062  ramcl  13076  firest  13337  mreexexd  13550  acsfn  13561  prslem  14065  ispos  14081  posi  14084  isposd  14089  lubval  14113  glbval  14118  joinval2  14123  meetval2  14130  pospropd  14238  spwval2  14333  spwpr2  14337  odlem1  14850  mndodcongi  14858  gexlem1  14890  sylow1lem3  14911  efgredlemb  15055  efgred  15057  frgpnabllem1  15161  isrrg  16029  mplsubglem  16179  mpllsslem  16180  ltbval  16213  opsrval  16216  xrsdsreclb  16418  istopg  16641  isclo2  16825  lmbr  16988  ist0  17048  ist1-2  17075  t1sep2  17097  cmpfi  17135  2ndcdisj  17182  1stccn  17189  iskgen3  17244  ptpjopn  17306  hausdiag  17339  xkopt  17349  ist0-4  17420  isr0  17428  r0sep  17439  fbfinnfr  17536  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  cnflf  17697  cnfcf  17737  tmdgsum2  17779  tsmsgsum  17821  tsmsres  17826  tsmsf1o  17827  tsmsxplem1  17835  tsmsxp  17837  metcnp  18087  metcnpi3  18092  txmetcnp  18093  ngptgp  18152  nlmvscnlem1  18197  nrginvrcnlem  18201  nghmcn  18254  xrge0tsms  18339  xmetdcn2  18342  metdscn  18360  addcnlem  18368  elcncf1di  18399  ipcnlem1  18672  caucfil  18709  metcld  18731  metcld2  18732  volcn  18961  itg2cnlem2  19117  ellimc2  19227  dveflem  19326  dvne0  19358  mdegleb  19450  mdegle0  19463  ply1divex  19522  fta1g  19553  dgrco  19656  plydivex  19677  fta1  19688  vieta1  19692  abelthlem8  19815  divlogrlim  19982  cxpcn3lem  20087  rlimcnp  20260  cxplim  20266  cxploglim  20272  ftalem1  20310  ftalem2  20311  dvdsmulf1o  20434  ppiublem1  20441  dchrinv  20500  lgseisenlem2  20589  2sqlem6  20608  2sqlem8  20611  2sqlem10  20613  dchrisum0  20669  rngoidmlem  21090  isnvlem  21166  vacn  21267  nmcvcn  21268  smcnlem  21270  blocni  21383  norm3lemt  21731  isch2  21803  chlimi  21814  omlsii  21982  eigorth  22418  0cnop  22559  0cnfn  22560  idcnop  22561  lnconi  22613  stcltr1i  22854  elat2  22920  funcnv5mpt  23236  xrge0tsmsd  23382  erdszelem8  23729  ghomf1olem  24001  climuzcnv  24004  relexpindlem  24036  relexpind  24037  rtrclreclem.trans  24043  rtrclind  24046  poseq  24253  frrlem4  24284  nocvxminlem  24344  elfuns  24454  axlowdimlem15  24584  ifscgr  24667  idinside  24707  brsegle  24731  alexeqd  24962  cbcpcp  25162  isorhom  25211  preoref22  25229  mxlelt  25264  mnlelt2  25266  ablocomgrp  25342  glmrngo  25482  intopcoaconlem3b  25538  islimrs3  25581  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  ismona  25809  ismonb  25810  imonclem  25813  isepia  25819  isepib  25820  iepiclem  25823  setiscat  25979  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibcg  26191  trer  26227  filnetlem4  26330  filbcmb  26432  sdclem2  26452  fdc  26455  fdc1  26456  divrngidl  26653  pridlval  26658  smprngopr  26677  ralxpxfr2d  26760  aomclem8  27159  islindf4  27308  hbtlem5  27332  acsfn1p  27507  2sbc6g  27615  sbiota1  27634  wallispilem3  27816  bnj1145  29023  bnj1171  29030  bnj1172  29031  isat3  29497  iscvlat2N  29514  psubspset  29933  ldilfset  30297  ldilset  30298  dilfsetN  30341  dilsetN  30342  cdlemefrs29bpre0  30585  cdlemefrs29clN  30588  cdlemefrs32fva  30589  cdlemn11pre  31400  dihord2pre  31415  lpolsetN  31672
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 177
  Copyright terms: Public domain W3C validator