MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi1d Structured version   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  1702  19.21t  1813  ax11v2  2078  ax11v2OLD  2079  drsb1  2112  ax11vALT  2173  ax11inda  2277  ax11v2-o  2278  ralcom2  2872  raleqf  2900  alexeq  3065  mo2icl  3113  sbc19.21g  3225  csbiebg  3290  ralss  3409  r19.37zv  3724  ssuni  4037  intmin4  4079  ssexg  4349  pocl  4510  ordunisuc2  4824  tfisi  4838  tfinds  4839  tfindsg  4840  tfindsg2  4841  dfom2  4847  findsg  4872  vtoclr  4922  frsn  4948  fun11  5516  funimass4  5777  dff13  6004  f1mpt  6007  isopolem  6065  oprabid  6105  caovcan  6251  caoftrn  6339  frxp  6456  dfsmo2  6609  qliftfun  6989  ecoptocl  6994  ecopovtrn  7007  dom2lem  7147  findcard  7347  findcard2  7348  findcard3  7350  fiint  7383  supmo  7457  eqsup  7461  suplub  7465  supmaxlem  7469  supisoex  7476  wemaplem1  7515  wemaplem2  7516  wemapso2lem  7519  oemapvali  7640  cantnf  7649  wemapwe  7654  karden  7819  aceq1  7998  zorn2lem1  8376  axrepndlem2  8468  axregndlem2  8478  pwfseqlem4  8537  gruurn  8673  indpi  8784  nqereu  8806  prcdnq  8870  supexpr  8931  ltsosr  8969  supsrlem  8986  supsr  8987  axpre-lttrn  9041  axpre-sup  9044  prodgt0  9855  infm3  9967  prime  10350  raluz  10525  zsupss  10565  uzsupss  10568  xrsupsslem  10885  xrinfmsslem  10886  fz1sbc  11124  brfi1uzind  11715  wrdind  11791  rexanre  12150  rexico  12157  limsupgle  12271  rlim2lt  12291  rlim3  12292  ello12  12310  ello12r  12311  ello1d  12317  elo12  12321  elo12r  12322  rlimconst  12338  lo1resb  12358  o1resb  12360  rlimcn2  12384  addcn2  12387  mulcn2  12389  reccn2  12390  cn1lem  12391  o1rlimmul  12412  lo1le  12445  caucvgrlem  12466  divrcnv  12632  rpnnen2  12825  sqr2irr  12848  exprmfct  13110  isprm5  13112  prmdvdsexpr  13116  prmpwdvds  13272  vdwmc2  13347  ramtlecl  13368  ramub  13381  rami  13383  ramcl  13397  firest  13660  mreexexd  13873  acsfn  13884  prslem  14388  ispos  14404  posi  14407  isposd  14412  lubval  14436  glbval  14441  joinval2  14446  meetval2  14453  pospropd  14561  spwval2  14656  spwpr2  14660  odlem1  15173  mndodcongi  15181  gexlem1  15213  sylow1lem3  15234  efgredlemb  15378  efgred  15380  frgpnabllem1  15484  isrrg  16348  mplsubglem  16498  mpllsslem  16499  ltbval  16532  opsrval  16535  xrsdsreclb  16745  istopg  16968  isclo2  17152  neiptoptop  17195  neiptopnei  17196  lmbr  17322  ist0  17384  ist1-2  17411  t1sep2  17433  cmpfi  17471  2ndcdisj  17519  1stccn  17526  iskgen3  17581  ptpjopn  17644  hausdiag  17677  xkopt  17687  ist0-4  17761  isr0  17769  r0sep  17780  fbfinnfr  17873  fmfnfmlem2  17987  fmfnfmlem4  17989  fmfnfm  17990  cnflf  18034  cnfcf  18074  tmdgsum2  18126  tsmsgsum  18168  tsmsres  18173  tsmsf1o  18174  tsmsxplem1  18182  tsmsxp  18184  ustssel  18235  ustincl  18237  ustdiag  18238  ustinvel  18239  ustexhalf  18240  ust0  18249  ustuqtop4  18274  utopsnneiplem  18277  isucn2  18309  iducn  18313  metcnp  18571  metcnpi3  18576  txmetcnp  18577  metucnOLD  18618  metucn  18619  ngptgp  18677  nlmvscnlem1  18722  nrginvrcnlem  18726  nghmcn  18779  xrge0tsms  18865  xmetdcn2  18868  metdscn  18886  addcnlem  18894  elcncf1di  18925  ipcnlem1  19199  caucfil  19236  metcld  19258  metcld2  19259  volcn  19498  itg2cnlem2  19654  ellimc2  19764  dveflem  19863  dvne0  19895  mdegleb  19987  mdegle0  20000  ply1divex  20059  fta1g  20090  dgrco  20193  plydivex  20214  fta1  20225  vieta1  20229  abelthlem8  20355  divlogrlim  20526  cxpcn3lem  20631  rlimcnp  20804  cxplim  20810  cxploglim  20816  ftalem1  20855  ftalem2  20856  dvdsmulf1o  20979  ppiublem1  20986  dchrinv  21045  lgseisenlem2  21134  2sqlem6  21153  2sqlem8  21156  2sqlem10  21158  dchrisum0  21214  3v3e3cycl1  21631  constr3trllem2  21638  4cycl4v4e  21653  4cycl4dv4e  21655  eupatrl  21690  rngoidmlem  22011  isnvlem  22089  vacn  22190  nmcvcn  22191  smcnlem  22193  blocni  22306  norm3lemt  22654  isch2  22726  chlimi  22737  omlsii  22905  eigorth  23341  0cnop  23482  0cnfn  23483  idcnop  23484  lnconi  23536  stcltr1i  23777  elat2  23843  funcnv5mpt  24084  resspos  24187  xrge0tsmsd  24223  qqhcn  24375  qqhucn  24376  erdszelem8  24884  ghomf1olem  25105  climuzcnv  25108  relexpindlem  25139  relexpind  25140  rtrclreclem.trans  25146  rtrclind  25149  poseq  25528  frrlem4  25585  nocvxminlem  25645  axlowdimlem15  25895  ifscgr  25978  idinside  26018  brsegle  26042  mbfresfi  26253  itg2addnc  26259  ftc1anc  26288  trer  26319  filnetlem4  26410  filbcmb  26442  sdclem2  26446  fdc  26449  fdc1  26450  divrngidl  26638  pridlval  26643  smprngopr  26662  ralxpxfr2d  26741  aomclem8  27136  islindf4  27285  hbtlem5  27309  acsfn1p  27484  2sbc6g  27592  sbiota1  27611  wallispilem3  27792  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  frgrawopreglem2  28434  usg2spot2nb  28454  bnj1145  29362  bnj1171  29369  bnj1172  29370  drsb1NEW7  29506  ax11v2NEW7  29530  isat3  30105  iscvlat2N  30122  psubspset  30541  ldilfset  30905  ldilset  30906  dilfsetN  30949  dilsetN  30950  cdlemefrs29bpre0  31193  cdlemefrs29clN  31196  cdlemefrs32fva  31197  cdlemn11pre  32008  dihord2pre  32023  lpolsetN  32280
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