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

Theorem imbi1d 308
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 214 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 69 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 198 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 69 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 183 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12d  311  imbi1  313  imim21b  356  pm5.33  848  con3th  924  ax12bOLD  1675  ax11v2  1945  drsb1  1975  ax11inda  2152  ax11v2-o  2153  ralcom2  2717  raleqf  2745  alexeq  2910  mo2icl  2957  sbc19.21g  3068  csbiebg  3133  ralss  3252  r19.37zv  3563  ssuni  3865  intmin4  3907  ssexg  4176  pocl  4337  ordunisuc2  4651  tfisi  4665  tfinds  4666  tfindsg  4667  tfindsg2  4668  dfom2  4674  findsg  4699  vtoclr  4749  frsn  4776  fun11  5331  funimass4  5589  dff13  5799  f1mpt  5801  isopolem  5858  oprabid  5898  caovcan  6040  caoftrn  6128  frxp  6241  dfsmo2  6380  qliftfun  6759  ecoptocl  6764  ecopovtrn  6777  dom2lem  6917  findcard  7113  findcard2  7114  findcard3  7116  fiint  7149  supmo  7219  eqsup  7223  suplub  7227  supmaxlem  7231  supisoex  7238  wemaplem1  7277  wemaplem2  7278  wemapso2lem  7281  oemapvali  7402  cantnf  7411  wemapwe  7416  karden  7581  aceq1  7760  zorn2lem1  8139  axrepndlem2  8231  axregndlem2  8241  pwfseqlem4  8300  gruurn  8436  indpi  8547  nqereu  8569  prcdnq  8633  supexpr  8694  ltsosr  8732  supsrlem  8749  supsr  8750  axpre-lttrn  8804  axpre-sup  8807  prodgt0  9617  lbinfm  9723  infm3  9729  prime  10108  raluz  10283  zsupss  10323  uzsupss  10326  xrsupsslem  10641  xrinfmsslem  10642  fz1sbc  10875  wrdind  11493  rexanre  11846  rexico  11853  limsupgle  11967  rlim2lt  11987  rlim3  11988  ello12  12006  ello12r  12007  ello1d  12013  elo12  12017  elo12r  12018  rlimconst  12034  lo1resb  12054  o1resb  12056  rlimcn2  12080  addcn2  12083  mulcn2  12085  reccn2  12086  cn1lem  12087  o1rlimmul  12108  lo1le  12141  caucvgrlem  12161  divrcnv  12327  rpnnen2  12520  sqr2irr  12543  exprmfct  12805  isprm5  12807  prmdvdsexpr  12811  prmpwdvds  12967  vdwmc2  13042  ramtlecl  13063  ramub  13076  rami  13078  ramcl  13092  firest  13353  mreexexd  13566  acsfn  13577  prslem  14081  ispos  14097  posi  14100  isposd  14105  lubval  14129  glbval  14134  joinval2  14139  meetval2  14146  pospropd  14254  spwval2  14349  spwpr2  14353  odlem1  14866  mndodcongi  14874  gexlem1  14906  sylow1lem3  14927  efgredlemb  15071  efgred  15073  frgpnabllem1  15177  isrrg  16045  mplsubglem  16195  mpllsslem  16196  ltbval  16229  opsrval  16232  xrsdsreclb  16434  istopg  16657  isclo2  16841  lmbr  17004  ist0  17064  ist1-2  17091  t1sep2  17113  cmpfi  17151  2ndcdisj  17198  1stccn  17205  iskgen3  17260  ptpjopn  17322  hausdiag  17355  xkopt  17365  ist0-4  17436  isr0  17444  r0sep  17455  fbfinnfr  17552  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  cnflf  17713  cnfcf  17753  tmdgsum2  17795  tsmsgsum  17837  tsmsres  17842  tsmsf1o  17843  tsmsxplem1  17851  tsmsxp  17853  metcnp  18103  metcnpi3  18108  txmetcnp  18109  ngptgp  18168  nlmvscnlem1  18213  nrginvrcnlem  18217  nghmcn  18270  xrge0tsms  18355  xmetdcn2  18358  metdscn  18376  addcnlem  18384  elcncf1di  18415  ipcnlem1  18688  caucfil  18725  metcld  18747  metcld2  18748  volcn  18977  itg2cnlem2  19133  ellimc2  19243  dveflem  19342  dvne0  19374  mdegleb  19466  mdegle0  19479  ply1divex  19538  fta1g  19569  dgrco  19672  plydivex  19693  fta1  19704  vieta1  19708  abelthlem8  19831  divlogrlim  19998  cxpcn3lem  20103  rlimcnp  20276  cxplim  20282  cxploglim  20288  ftalem1  20326  ftalem2  20327  dvdsmulf1o  20450  ppiublem1  20457  dchrinv  20516  lgseisenlem2  20605  2sqlem6  20624  2sqlem8  20627  2sqlem10  20629  dchrisum0  20685  rngoidmlem  21106  isnvlem  21182  vacn  21283  nmcvcn  21284  smcnlem  21286  blocni  21399  norm3lemt  21747  isch2  21819  chlimi  21830  omlsii  21998  eigorth  22434  0cnop  22575  0cnfn  22576  idcnop  22577  lnconi  22629  stcltr1i  22870  elat2  22936  funcnv5mpt  23251  xrge0tsmsd  23397  erdszelem8  23744  ghomf1olem  24016  climuzcnv  24019  relexpindlem  24051  relexpind  24052  rtrclreclem.trans  24058  rtrclind  24061  faclimlem5  24121  poseq  24324  frrlem4  24355  nocvxminlem  24415  elfuns  24525  axlowdimlem15  24656  ifscgr  24739  idinside  24779  brsegle  24803  alexeqd  25065  cbcpcp  25265  isorhom  25314  preoref22  25332  mxlelt  25367  mnlelt2  25369  ablocomgrp  25445  glmrngo  25585  intopcoaconlem3b  25641  islimrs3  25684  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  ismona  25912  ismonb  25913  imonclem  25916  isepia  25922  isepib  25923  iepiclem  25926  setiscat  26082  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibcg  26294  trer  26330  filnetlem4  26433  filbcmb  26535  sdclem2  26555  fdc  26558  fdc1  26559  divrngidl  26756  pridlval  26761  smprngopr  26780  ralxpxfr2d  26863  aomclem8  27262  islindf4  27411  hbtlem5  27435  acsfn1p  27610  2sbc6g  27718  sbiota1  27737  wallispilem3  27919  eupatrl  28385  3v3e3cycl1  28390  constr3trllem2  28397  4cycl4v4e  28412  4cycl4dv4e  28414  bnj1145  29339  bnj1171  29346  bnj1172  29347  drsb1NEW7  29483  ax11v2NEW7  29505  isat3  30119  iscvlat2N  30136  psubspset  30555  ldilfset  30919  ldilset  30920  dilfsetN  30963  dilsetN  30964  cdlemefrs29bpre0  31207  cdlemefrs29clN  31210  cdlemefrs32fva  31211  cdlemn11pre  32022  dihord2pre  32037  lpolsetN  32294
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 177
  Copyright terms: Public domain W3C validator