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, 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 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  878  con3th  958  ax12vOLD  1842  19.21t  1890  ax12v2  2069  drsb1  2104  ax12inda  2264  ax12v2-o  2265  ralcom2  3008  raleqf  3036  ralxpxfr2d  3210  alexeqg  3214  alexeq  3215  mo2icl  3264  sbc19.21g  3386  csbiebg  3443  ralss  3551  r19.37zv  3911  ssuni  4256  intmin4  4301  ssexg  4583  pocl  4797  vtoclr  5034  frsn  5060  fun11  5643  funimass4  5909  dff13  6151  f1mpt  6154  isopolem  6226  oprabid  6308  caovcan  6464  caoftrn  6560  ordunisuc2  6664  tfisi  6678  tfinds  6679  tfindsg  6680  tfindsg2  6681  dfom2  6687  findsg  6712  frxp  6895  dfsmo2  7020  qliftfun  7398  ecoptocl  7403  ecopovtrn  7416  dom2lem  7557  findcard  7761  findcard2  7762  findcard3  7765  fiint  7799  supmo  7914  eqsup  7918  suplub  7922  supmaxlemOLD  7927  supisoex  7935  wemaplem1  7974  wemaplem2  7975  wemapsolem  7978  oemapvali  8106  cantnf  8115  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  karden  8316  aceq1  8501  zorn2lem1  8879  axrepndlem2  8971  axregndlem2  8983  pwfseqlem4  9043  gruurn  9179  indpi  9288  nqereu  9310  prcdnq  9374  supexpr  9435  ltsosr  9474  supsrlem  9491  supsr  9492  axpre-lttrn  9546  axpre-sup  9549  prodgt0  10394  infm3  10509  prime  10950  raluz  11139  zsupss  11181  uzsupss  11184  xrsupsslem  11508  xrinfmsslem  11509  fz1sbc  11764  ssnn0fi  12075  brfi1uzind  12513  wrdind  12683  wrd2ind  12684  rexanre  13160  rexico  13167  limsupgle  13281  rlim2lt  13301  rlim3  13302  ello12  13320  ello12r  13321  ello1d  13327  elo12  13331  elo12r  13332  rlimconst  13348  lo1resb  13368  o1resb  13370  rlimcn2  13394  addcn2  13397  mulcn2  13399  reccn2  13400  cn1lem  13401  o1rlimmul  13422  lo1le  13455  caucvgrlem  13476  divrcnv  13645  rpnnen2  13940  sqrt2irr  13963  exprmfct  14232  isprm5  14234  prmdvdsexpr  14238  prmpwdvds  14403  vdwmc2  14478  ramtlecl  14499  ramub  14512  rami  14514  ramcl  14528  firest  14811  mreexexd  15026  acsfn  15037  prslem  15538  ispos  15554  posi  15557  isposd  15563  lubeldm  15589  lubval  15592  glbeldm  15602  glbval  15605  joinval2lem  15616  meetval2lem  15630  pospropd  15742  odlem1  16537  mndodcongi  16545  gexlem1  16577  sylow1lem3  16598  efgredlemb  16742  efgred  16744  frgpnabllem1  16855  isrrg  17914  mplsubglem  18071  mpllsslem  18072  mplsubglemOLD  18073  mpllsslemOLD  18074  ltbval  18114  opsrval  18117  xrsdsreclb  18443  islindf4  18850  mdetunilem1  19091  mdetunilem3  19093  mdetunilem4  19094  mdetunilem9  19099  chpscmat  19320  chfacffsupp  19334  chfacfscmulfsupp  19337  chfacfpmmulfsupp  19341  istopg  19381  isclo2  19566  neiptoptop  19609  neiptopnei  19610  lmbr  19736  ist0  19798  ist1-2  19825  t1sep2  19847  cmpfi  19885  2ndcdisj  19934  1stccn  19941  iskgen3  20027  ptpjopn  20090  hausdiag  20123  xkopt  20133  ist0-4  20207  isr0  20215  r0sep  20226  fbfinnfr  20319  fmfnfmlem2  20433  fmfnfmlem4  20435  fmfnfm  20436  cnflf  20480  cnfcf  20520  tmdgsum2  20572  tsmsgsum  20614  tsmsgsumOLD  20617  tsmsresOLD  20622  tsmsres  20623  tsmsf1o  20624  tsmsxplem1  20632  tsmsxp  20634  ustssel  20685  ustincl  20687  ustdiag  20688  ustinvel  20689  ustexhalf  20690  ust0  20699  ustuqtop4  20724  utopsnneiplem  20727  isucn2  20759  iducn  20763  metcnp  21021  metcnpi3  21026  txmetcnp  21027  metucnOLD  21068  metucn  21069  ngptgp  21127  nlmvscnlem1  21172  nrginvrcnlem  21176  nghmcn  21229  xrge0tsms  21316  xmetdcn2  21319  metdscn  21337  addcnlem  21345  elcncf1di  21376  ipcnlem1  21662  caucfil  21699  metcld  21721  metcld2  21722  volcn  21992  itg2cnlem2  22146  ellimc2  22258  dveflem  22357  dvne0  22389  mdegleb  22441  mdegle0  22454  ply1divex  22514  fta1g  22545  dgrco  22648  plydivex  22669  fta1  22680  vieta1  22684  abelthlem8  22810  divlogrlim  22992  cxpcn3lem  23097  rlimcnp  23271  cxplim  23277  cxploglim  23283  ftalem1  23322  ftalem2  23323  dvdsmulf1o  23446  ppiublem1  23453  dchrinv  23512  lgseisenlem2  23601  2sqlem6  23620  2sqlem8  23623  2sqlem10  23625  dchrisum0  23681  istrkgc  23827  istrkgb  23828  axtgcgrid  23836  axtg5seg  23838  axtgpasch  23840  axtgupdim2  23845  axtgeucl  23846  axlowdimlem15  24235  usgra2wlkspthlem1  24595  usgra2wlkspthlem2  24596  3v3e3cycl1  24620  constr3trllem2  24627  4cycl4v4e  24642  4cycl4dv4e  24644  eupatrl  24944  frgrawopreglem2  25021  usg2spot2nb  25041  friendshipgt3  25097  rngoidmlem  25401  isnvlem  25479  vacn  25580  nmcvcn  25581  smcnlem  25583  blocni  25696  norm3lemt  26045  isch2  26117  chlimi  26128  omlsii  26297  eigorth  26733  0cnop  26874  0cnfn  26875  idcnop  26876  lnconi  26928  stcltr1i  27169  elat2  27235  funcnv5mpt  27487  xrge0infss  27556  resspos  27624  xrge0tsmsd  27752  qqhcn  27949  qqhucn  27950  eulerpartlemgvv  28292  sgn3da  28457  sgnnbi  28461  sgnpbi  28462  erdszelem8  28619  mclsval  28900  mclsax  28906  mclsppslem  28920  ghomf1olem  29011  climuzcnv  29014  relexpindlem  29039  relexpind  29040  rtrclreclem.trans  29046  rtrclind  29049  poseq  29308  frrlem4  29365  nocvxminlem  29425  ifscgr  29669  idinside  29709  brsegle  29733  wl-sbrimt  29973  fin2so  30015  heicant  30024  mbfresfi  30036  itg2addnc  30044  ftc1anc  30073  trer  30109  filnetlem4  30174  filbcmb  30206  sdclem2  30210  fdc  30213  fdc1  30214  divrngidl  30400  pridlval  30405  smprngopr  30424  aomclem8  30982  hbtlem5  31052  acsfn1p  31124  isprm7  31168  2sbc6g  31276  sbiota1  31295  mullimc  31530  limcdm0  31532  mullimcf  31537  constlimc  31538  idlimc  31540  limsupre  31555  limcleqr  31558  addlimc  31562  0ellimcdiv  31563  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  wallispilem3  31738  fourierdlem48  31826  fourierdlem87  31865  usgra2pthspth  32189  usgra2pthlem1  32191  ply1mulgsumlem1  32721  ply1mulgsumlem2  32722  bnj1145  33782  bnj1171  33789  bnj1172  33790  bj-con3ALT  33909  bj-axc15v  34078  bj-19.21t  34151  isat3  34772  iscvlat2N  34789  psubspset  35208  ldilfset  35572  ldilset  35573  dilfsetN  35617  dilsetN  35618  cdlemefrs29bpre0  35862  cdlemefrs29clN  35865  cdlemefrs32fva  35866  cdlemn11pre  36677  dihord2pre  36692  lpolsetN  36949
  Copyright terms: Public domain W3C validator