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, 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 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  866  con3th  942  19.21t  1836  ax12v2  2032  drsb1  2065  ax12vALT  2133  ax12inda  2250  ax12v2-o  2251  ralcom2  2875  raleqf  2903  ralxpxfr2d  3073  alexeqg  3077  alexeq  3078  mo2icl  3127  sbc19.21g  3247  csbiebg  3299  ralss  3406  r19.37zv  3764  ssuni  4101  intmin4  4145  ssexg  4426  pocl  4635  vtoclr  4870  frsn  4896  fun11  5471  funimass4  5730  dff13  5958  f1mpt  5961  isopolem  6023  oprabid  6104  caovcan  6256  caoftrn  6344  ordunisuc2  6444  tfisi  6458  tfinds  6459  tfindsg  6460  tfindsg2  6461  dfom2  6467  findsg  6492  frxp  6671  dfsmo2  6794  qliftfun  7173  ecoptocl  7178  ecopovtrn  7191  dom2lem  7337  findcard  7539  findcard2  7540  findcard3  7543  fiint  7576  supmo  7690  eqsup  7694  suplub  7698  supmaxlem  7702  supisoex  7709  wemaplem1  7748  wemaplem2  7749  wemapsolem  7752  oemapvali  7880  cantnf  7889  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  karden  8090  aceq1  8275  zorn2lem1  8653  axrepndlem2  8745  axregndlem2  8757  pwfseqlem4  8816  gruurn  8952  indpi  9063  nqereu  9085  prcdnq  9149  supexpr  9210  ltsosr  9248  supsrlem  9265  supsr  9266  axpre-lttrn  9320  axpre-sup  9323  prodgt0  10161  infm3  10276  prime  10709  raluz  10890  zsupss  10931  uzsupss  10934  xrsupsslem  11256  xrinfmsslem  11257  fz1sbc  11519  brfi1uzind  12202  wrdind  12354  wrd2ind  12355  rexanre  12817  rexico  12824  limsupgle  12938  rlim2lt  12958  rlim3  12959  ello12  12977  ello12r  12978  ello1d  12984  elo12  12988  elo12r  12989  rlimconst  13005  lo1resb  13025  o1resb  13027  rlimcn2  13051  addcn2  13054  mulcn2  13056  reccn2  13057  cn1lem  13058  o1rlimmul  13079  lo1le  13112  caucvgrlem  13133  divrcnv  13297  rpnnen2  13490  sqr2irr  13513  exprmfct  13778  isprm5  13780  prmdvdsexpr  13784  prmpwdvds  13947  vdwmc2  14022  ramtlecl  14043  ramub  14056  rami  14058  ramcl  14072  firest  14353  mreexexd  14568  acsfn  14579  prslem  15083  ispos  15099  posi  15102  isposd  15107  lubeldm  15133  lubval  15136  glbeldm  15146  glbval  15149  joinval2lem  15160  meetval2lem  15174  pospropd  15286  odlem1  16017  mndodcongi  16025  gexlem1  16057  sylow1lem3  16078  efgredlemb  16222  efgred  16224  frgpnabllem1  16330  isrrg  17280  mplsubglem  17443  mpllsslem  17444  mplsubglemOLD  17445  mpllsslemOLD  17446  ltbval  17484  opsrval  17487  xrsdsreclb  17703  islindf4  18108  mdetunilem1  18259  mdetunilem3  18261  mdetunilem4  18262  mdetunilem9  18267  istopg  18349  isclo2  18533  neiptoptop  18576  neiptopnei  18577  lmbr  18703  ist0  18765  ist1-2  18792  t1sep2  18814  cmpfi  18852  2ndcdisj  18901  1stccn  18908  iskgen3  18963  ptpjopn  19026  hausdiag  19059  xkopt  19069  ist0-4  19143  isr0  19151  r0sep  19162  fbfinnfr  19255  fmfnfmlem2  19369  fmfnfmlem4  19371  fmfnfm  19372  cnflf  19416  cnfcf  19456  tmdgsum2  19508  tsmsgsum  19550  tsmsgsumOLD  19553  tsmsresOLD  19558  tsmsres  19559  tsmsf1o  19560  tsmsxplem1  19568  tsmsxp  19570  ustssel  19621  ustincl  19623  ustdiag  19624  ustinvel  19625  ustexhalf  19626  ust0  19635  ustuqtop4  19660  utopsnneiplem  19663  isucn2  19695  iducn  19699  metcnp  19957  metcnpi3  19962  txmetcnp  19963  metucnOLD  20004  metucn  20005  ngptgp  20063  nlmvscnlem1  20108  nrginvrcnlem  20112  nghmcn  20165  xrge0tsms  20252  xmetdcn2  20255  metdscn  20273  addcnlem  20281  elcncf1di  20312  ipcnlem1  20598  caucfil  20635  metcld  20657  metcld2  20658  volcn  20927  itg2cnlem2  21081  ellimc2  21193  dveflem  21292  dvne0  21324  mdegleb  21419  mdegle0  21432  ply1divex  21492  fta1g  21523  dgrco  21626  plydivex  21647  fta1  21658  vieta1  21662  abelthlem8  21788  divlogrlim  21964  cxpcn3lem  22069  rlimcnp  22243  cxplim  22249  cxploglim  22255  ftalem1  22294  ftalem2  22295  dvdsmulf1o  22418  ppiublem1  22425  dchrinv  22484  lgseisenlem2  22573  2sqlem6  22592  2sqlem8  22595  2sqlem10  22597  dchrisum0  22653  istrkgc  22801  istrkgb  22802  axtgcgrid  22808  axtg5seg  22810  axtgpasch  22812  axtgupdim2  22816  axtgeucl  22817  axlowdimlem15  23024  3v3e3cycl1  23352  constr3trllem2  23359  4cycl4v4e  23374  4cycl4dv4e  23376  eupatrl  23411  rngoidmlem  23732  isnvlem  23810  vacn  23911  nmcvcn  23912  smcnlem  23914  blocni  24027  norm3lemt  24376  isch2  24448  chlimi  24459  omlsii  24628  eigorth  25064  0cnop  25205  0cnfn  25206  idcnop  25207  lnconi  25259  stcltr1i  25500  elat2  25566  funcnv5mpt  25811  resspos  25942  xrge0tsmsd  26105  rngurd  26108  qqhcn  26273  qqhucn  26274  eulerpartlemgvv  26606  sgn3da  26771  sgnnbi  26775  sgnpbi  26776  erdszelem8  26933  ghomf1olem  27159  climuzcnv  27162  relexpindlem  27187  relexpind  27188  rtrclreclem.trans  27194  rtrclind  27197  poseq  27560  frrlem4  27617  nocvxminlem  27677  ifscgr  27921  idinside  27961  brsegle  27985  wl-sbrimt  28220  fin2so  28257  heicant  28267  mbfresfi  28279  itg2addnc  28287  ftc1anc  28316  trer  28352  filnetlem4  28443  filbcmb  28475  sdclem2  28479  fdc  28482  fdc1  28483  divrngidl  28669  pridlval  28674  smprngopr  28693  sbcom3OLD  28821  aomclem8  29256  hbtlem5  29326  acsfn1p  29398  2sbc6g  29511  sbiota1  29530  wallispilem3  29705  ccats1rev  30103  usgra2pthspth  30138  usgra2wlkspthlem1  30139  usgra2wlkspthlem2  30140  usgra2pthlem1  30143  frgrawopreglem2  30481  usg2spot2nb  30501  friendshipgt3  30557  bnj1145  31683  bnj1171  31690  bnj1172  31691  bj-axc15v  31893  bj-19.21t  31955  isat3  32522  iscvlat2N  32539  psubspset  32958  ldilfset  33322  ldilset  33323  dilfsetN  33366  dilsetN  33367  cdlemefrs29bpre0  33610  cdlemefrs29clN  33613  cdlemefrs32fva  33614  cdlemn11pre  34425  dihord2pre  34440  lpolsetN  34697
  Copyright terms: Public domain W3C validator