MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi1d 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  1698  19.21t  1809  ax11v2  2045  drsb1  2071  ax11vALT  2146  ax11inda  2250  ax11v2-o  2251  ralcom2  2832  raleqf  2860  alexeq  3025  mo2icl  3073  sbc19.21g  3185  csbiebg  3250  ralss  3369  r19.37zv  3684  ssuni  3997  intmin4  4039  ssexg  4309  pocl  4470  ordunisuc2  4783  tfisi  4797  tfinds  4798  tfindsg  4799  tfindsg2  4800  dfom2  4806  findsg  4831  vtoclr  4881  frsn  4907  fun11  5475  funimass4  5736  dff13  5963  f1mpt  5966  isopolem  6024  oprabid  6064  caovcan  6210  caoftrn  6298  frxp  6415  dfsmo2  6568  qliftfun  6948  ecoptocl  6953  ecopovtrn  6966  dom2lem  7106  findcard  7306  findcard2  7307  findcard3  7309  fiint  7342  supmo  7413  eqsup  7417  suplub  7421  supmaxlem  7425  supisoex  7432  wemaplem1  7471  wemaplem2  7472  wemapso2lem  7475  oemapvali  7596  cantnf  7605  wemapwe  7610  karden  7775  aceq1  7954  zorn2lem1  8332  axrepndlem2  8424  axregndlem2  8434  pwfseqlem4  8493  gruurn  8629  indpi  8740  nqereu  8762  prcdnq  8826  supexpr  8887  ltsosr  8925  supsrlem  8942  supsr  8943  axpre-lttrn  8997  axpre-sup  9000  prodgt0  9811  infm3  9923  prime  10306  raluz  10481  zsupss  10521  uzsupss  10524  xrsupsslem  10841  xrinfmsslem  10842  fz1sbc  11079  brfi1uzind  11670  wrdind  11746  rexanre  12105  rexico  12112  limsupgle  12226  rlim2lt  12246  rlim3  12247  ello12  12265  ello12r  12266  ello1d  12272  elo12  12276  elo12r  12277  rlimconst  12293  lo1resb  12313  o1resb  12315  rlimcn2  12339  addcn2  12342  mulcn2  12344  reccn2  12345  cn1lem  12346  o1rlimmul  12367  lo1le  12400  caucvgrlem  12421  divrcnv  12587  rpnnen2  12780  sqr2irr  12803  exprmfct  13065  isprm5  13067  prmdvdsexpr  13071  prmpwdvds  13227  vdwmc2  13302  ramtlecl  13323  ramub  13336  rami  13338  ramcl  13352  firest  13615  mreexexd  13828  acsfn  13839  prslem  14343  ispos  14359  posi  14362  isposd  14367  lubval  14391  glbval  14396  joinval2  14401  meetval2  14408  pospropd  14516  spwval2  14611  spwpr2  14615  odlem1  15128  mndodcongi  15136  gexlem1  15168  sylow1lem3  15189  efgredlemb  15333  efgred  15335  frgpnabllem1  15439  isrrg  16303  mplsubglem  16453  mpllsslem  16454  ltbval  16487  opsrval  16490  xrsdsreclb  16700  istopg  16923  isclo2  17107  neiptoptop  17150  neiptopnei  17151  lmbr  17276  ist0  17338  ist1-2  17365  t1sep2  17387  cmpfi  17425  2ndcdisj  17472  1stccn  17479  iskgen3  17534  ptpjopn  17597  hausdiag  17630  xkopt  17640  ist0-4  17714  isr0  17722  r0sep  17733  fbfinnfr  17826  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  cnflf  17987  cnfcf  18027  tmdgsum2  18079  tsmsgsum  18121  tsmsres  18126  tsmsf1o  18127  tsmsxplem1  18135  tsmsxp  18137  ustssel  18188  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ust0  18202  ustuqtop4  18227  utopsnneiplem  18230  isucn2  18262  iducn  18266  metcnp  18524  metcnpi3  18529  txmetcnp  18530  metucnOLD  18571  metucn  18572  ngptgp  18630  nlmvscnlem1  18675  nrginvrcnlem  18679  nghmcn  18732  xrge0tsms  18818  xmetdcn2  18821  metdscn  18839  addcnlem  18847  elcncf1di  18878  ipcnlem1  19152  caucfil  19189  metcld  19211  metcld2  19212  volcn  19451  itg2cnlem2  19607  ellimc2  19717  dveflem  19816  dvne0  19848  mdegleb  19940  mdegle0  19953  ply1divex  20012  fta1g  20043  dgrco  20146  plydivex  20167  fta1  20178  vieta1  20182  abelthlem8  20308  divlogrlim  20479  cxpcn3lem  20584  rlimcnp  20757  cxplim  20763  cxploglim  20769  ftalem1  20808  ftalem2  20809  dvdsmulf1o  20932  ppiublem1  20939  dchrinv  20998  lgseisenlem2  21087  2sqlem6  21106  2sqlem8  21109  2sqlem10  21111  dchrisum0  21167  3v3e3cycl1  21584  constr3trllem2  21591  4cycl4v4e  21606  4cycl4dv4e  21608  eupatrl  21643  rngoidmlem  21964  isnvlem  22042  vacn  22143  nmcvcn  22144  smcnlem  22146  blocni  22259  norm3lemt  22607  isch2  22679  chlimi  22690  omlsii  22858  eigorth  23294  0cnop  23435  0cnfn  23436  idcnop  23437  lnconi  23489  stcltr1i  23730  elat2  23796  funcnv5mpt  24037  resspos  24140  xrge0tsmsd  24176  qqhcn  24328  qqhucn  24329  erdszelem8  24837  ghomf1olem  25058  climuzcnv  25061  relexpindlem  25092  relexpind  25093  rtrclreclem.trans  25099  rtrclind  25102  poseq  25467  frrlem4  25498  nocvxminlem  25558  elfuns  25668  axlowdimlem15  25799  ifscgr  25882  idinside  25922  brsegle  25946  mbfresfi  26152  itg2addnc  26158  trer  26209  filnetlem4  26300  filbcmb  26332  sdclem2  26336  fdc  26339  fdc1  26340  divrngidl  26528  pridlval  26533  smprngopr  26552  ralxpxfr2d  26631  aomclem8  27027  islindf4  27176  hbtlem5  27200  acsfn1p  27375  2sbc6g  27483  sbiota1  27502  wallispilem3  27683  swrdccatin2  28018  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  frgrawopreglem2  28148  usg2spot2nb  28168  bnj1145  29068  bnj1171  29075  bnj1172  29076  drsb1NEW7  29212  ax11v2NEW7  29234  isat3  29790  iscvlat2N  29807  psubspset  30226  ldilfset  30590  ldilset  30591  dilfsetN  30634  dilsetN  30635  cdlemefrs29bpre0  30878  cdlemefrs29clN  30881  cdlemefrs32fva  30882  cdlemn11pre  31693  dihord2pre  31708  lpolsetN  31965
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