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

Theorem imbi1d 318
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 226 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 78 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 210 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 78 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 193 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  imbi12d  321  imbi1  324  imim21b  368  pm5.33  886  con3th  966  ax12vOLD  1906  19.21t  1958  ax12v2  2136  drsb1  2169  ralcom2  2991  raleqf  3019  ralxpxfr2d  3193  alexeqg  3197  alexeq  3198  mo2icl  3247  sbc19.21g  3361  csbiebg  3415  ralss  3524  r19.37zv  3890  ssuni  4235  intmin4  4279  ssexg  4563  pocl  4774  vtoclr  4891  frsn  4917  fun11  5658  funimass4  5924  dff13  6166  f1mpt  6169  isopolem  6243  oprabid  6324  caovcan  6479  caoftrn  6572  ordunisuc2  6677  tfisi  6691  tfinds  6692  tfindsg  6693  tfindsg2  6694  dfom2  6700  findsg  6726  frxp  6909  dfsmo2  7066  qliftfun  7448  ecoptocl  7453  ecopovtrn  7466  dom2lem  7608  findcard  7808  findcard2  7809  findcard3  7812  fiint  7846  supmo  7964  eqsup  7968  suplub  7972  supmaxlemOLD  7980  supisoex  7988  infmo  8009  wemaplem1  8059  wemaplem2  8060  wemapsolem  8063  oemapvali  8186  cantnf  8195  wemapwe  8199  karden  8363  aceq1  8544  zorn2lem1  8922  axrepndlem2  9014  axregndlem2  9024  pwfseqlem4  9083  gruurn  9219  indpi  9328  nqereu  9350  prcdnq  9414  supexpr  9475  ltsosr  9514  supsrlem  9531  supsr  9532  axpre-lttrn  9586  axpre-sup  9589  prodgt0  10446  infm3  10564  prime  11012  raluz  11203  zsupss  11249  uzsupss  11252  xrsupsslem  11588  xrinfmsslem  11589  fz1sbc  11864  ssnn0fi  12190  brfi1uzind  12637  wrdind  12814  wrd2ind  12815  relexprelg  13080  rtrclreclem3  13102  relexpindlem  13105  relexpind  13106  rtrclind  13107  rexanre  13388  rexico  13395  limsupgle  13513  rlim2lt  13539  rlim3  13540  ello12  13558  ello12r  13559  ello1d  13565  elo12  13569  elo12r  13570  rlimconst  13586  lo1resb  13606  o1resb  13608  rlimcn2  13632  addcn2  13635  mulcn2  13637  reccn2  13638  cn1lem  13639  o1rlimmul  13660  lo1le  13693  caucvgrlem  13714  caucvgrlemOLD  13715  divrcnv  13888  rpnnen2  14256  sqrt2irr  14279  exprmfct  14626  isprm5  14629  prmdvdsexpr  14647  prmpwdvds  14826  vdwmc2  14907  ramtlecl  14929  ramub  14948  rami  14950  ramcl  14965  firest  15309  mreexexd  15532  acsfn  15543  prslem  16154  ispos  16170  posi  16173  isposd  16179  lubeldm  16205  lubval  16208  glbeldm  16218  glbval  16221  joinval2lem  16232  meetval2lem  16246  pospropd  16358  odlem1  17159  odlem1OLD  17162  mndodcongi  17170  gexlem1  17206  gexlem1OLD  17208  sylow1lem3  17230  efgredlemb  17374  efgred  17376  frgpnabllem1  17487  isrrg  18490  mplsubglem  18636  mpllsslem  18637  ltbval  18673  opsrval  18676  xrsdsreclb  18993  islindf4  19373  mdetunilem1  19614  mdetunilem3  19616  mdetunilem4  19617  mdetunilem9  19622  chpscmat  19843  chfacffsupp  19857  chfacfscmulfsupp  19860  chfacfpmmulfsupp  19864  istopg  19902  isclo2  20081  neiptoptop  20124  neiptopnei  20125  lmbr  20251  ist0  20313  ist1-2  20340  t1sep2  20362  cmpfi  20400  2ndcdisj  20448  1stccn  20455  iskgen3  20541  ptpjopn  20604  hausdiag  20637  xkopt  20647  ist0-4  20721  isr0  20729  r0sep  20740  fbfinnfr  20833  fmfnfmlem2  20947  fmfnfmlem4  20949  fmfnfm  20950  cnflf  20994  cnfcf  21034  tmdgsum2  21088  tsmsgsum  21130  tsmsres  21135  tsmsf1o  21136  tsmsxplem1  21144  tsmsxp  21146  ustssel  21197  ustincl  21199  ustdiag  21200  ustinvel  21201  ustexhalf  21202  ust0  21211  ustuqtop4  21236  utopsnneiplem  21239  isucn2  21271  iducn  21275  metcnp  21533  metcnpi3  21538  txmetcnp  21539  metucn  21563  ngptgp  21621  nlmvscnlem1  21666  nrginvrcnlem  21670  nghmcn  21743  xrge0tsms  21829  xmetdcn2  21832  metdscn  21850  metdscnOLD  21865  addcnlem  21873  elcncf1di  21904  ipcnlem1  22193  caucfil  22230  metcld  22252  metcld2  22253  volcn  22541  itg2cnlem2  22697  ellimc2  22809  dveflem  22908  dvne0  22940  mdegleb  22990  mdegle0  23003  ply1divex  23064  fta1g  23095  dgrco  23206  plydivex  23227  fta1  23238  vieta1  23242  abelthlem8  23371  divlogrlim  23557  cxpcn3lem  23664  rlimcnp  23868  cxplim  23874  cxploglim  23880  ftalem1  23974  ftalem2  23975  dvdsmulf1o  24100  ppiublem1  24107  dchrinv  24166  lgseisenlem2  24255  2sqlem6  24274  2sqlem8  24277  2sqlem10  24279  dchrisum0  24335  istrkgc  24479  istrkgb  24480  axtgcgrid  24488  axtg5seg  24490  axtgpasch  24492  axtgeucl  24497  tgcgr4  24553  axlowdimlem15  24963  usgra2wlkspthlem1  25323  usgra2wlkspthlem2  25324  3v3e3cycl1  25348  constr3trllem2  25355  4cycl4v4e  25370  4cycl4dv4e  25372  eupatrl  25672  frgrawopreglem2  25749  usg2spot2nb  25769  friendshipgt3  25825  rngoidmlem  26127  isnvlem  26205  vacn  26306  nmcvcn  26307  smcnlem  26309  blocni  26422  norm3lemt  26781  isch2  26852  chlimi  26863  omlsii  27032  eigorth  27467  0cnop  27608  0cnfn  27609  idcnop  27610  lnconi  27662  stcltr1i  27903  elat2  27969  funcnv5mpt  28253  xrge0infss  28325  xrge0infssOLD  28326  resspos  28407  xrge0tsmsd  28537  qqhcn  28784  qqhucn  28785  esum2d  28903  eulerpartlemgvv  29198  sgn3da  29401  sgnnbi  29405  sgnpbi  29406  axtgupdim2OLD  29474  bnj1145  29791  bnj1171  29798  bnj1172  29799  erdszelem8  29910  mclsval  30190  mclsax  30196  mclsppslem  30210  ghomf1olem  30301  climuzcnv  30304  poseq  30479  frrlem4  30505  nocvxminlem  30565  ifscgr  30797  idinside  30837  brsegle  30861  trer  30958  filnetlem4  31023  bj-con3thALT  31141  bj-axc15v  31311  bj-19.21t  31384  wl-sbrimt  31786  wl-ax12v3  31820  fin2so  31840  ptrecube  31848  poimirlem26  31874  poimirlem27  31875  heicant  31883  mbfresfi  31895  itg2addnc  31904  ftc1anc  31933  filbcmb  31975  sdclem2  31979  fdc  31982  fdc1  31983  divrngidl  32169  pridlval  32174  smprngopr  32193  ax12inda  32432  ax12v2-o  32433  isat3  32786  iscvlat2N  32803  psubspset  33222  ldilfset  33586  ldilset  33587  dilfsetN  33631  dilsetN  33632  cdlemefrs29bpre0  33876  cdlemefrs29clN  33879  cdlemefrs32fva  33880  cdlemn11pre  34691  dihord2pre  34706  lpolsetN  34963  aomclem8  35833  hbtlem5  35901  acsfn1p  35979  ifpbi1  36035  ifpbi12  36046  ifpbi13  36047  isprm7  36512  2sbc6g  36618  sbiota1  36637  uzwo4  37248  fsumiunss  37444  mullimc  37483  limcdm0  37485  mullimcf  37490  constlimc  37491  idlimc  37493  limsupre  37508  limsupreOLD  37509  limcleqr  37512  addlimc  37516  0ellimcdiv  37517  ioodvbdlimc1lem2  37591  ioodvbdlimc1lem2OLD  37593  ioodvbdlimc2lem  37595  ioodvbdlimc2lemOLD  37596  dvmptfprodlem  37606  wallispilem3  37716  fourierdlem48  37805  fourierdlem87  37844  sge0f1o  37979  sge0iunmptlemre  38012  sge0iunmpt  38015  bgoldbachlt  38526  tgoldbachlt  38529  usgra2pthspth  38727  usgra2pthlem1  38729  ply1mulgsumlem1  39242  ply1mulgsumlem2  39243  elbigo2  39428  elbigo2r  39429  aacllem  39605
  Copyright terms: Public domain W3C validator