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  2025  ax11v2OLD  2026  drsb1  2078  ax11vALT  2154  ax11inda  2258  ax11v2-o  2259  ralcom2  2840  raleqf  2868  alexeq  3033  mo2icl  3081  sbc19.21g  3193  csbiebg  3258  ralss  3377  r19.37zv  3692  ssuni  4005  intmin4  4047  ssexg  4317  pocl  4478  ordunisuc2  4791  tfisi  4805  tfinds  4806  tfindsg  4807  tfindsg2  4808  dfom2  4814  findsg  4839  vtoclr  4889  frsn  4915  fun11  5483  funimass4  5744  dff13  5971  f1mpt  5974  isopolem  6032  oprabid  6072  caovcan  6218  caoftrn  6306  frxp  6423  dfsmo2  6576  qliftfun  6956  ecoptocl  6961  ecopovtrn  6974  dom2lem  7114  findcard  7314  findcard2  7315  findcard3  7317  fiint  7350  supmo  7421  eqsup  7425  suplub  7429  supmaxlem  7433  supisoex  7440  wemaplem1  7479  wemaplem2  7480  wemapso2lem  7483  oemapvali  7604  cantnf  7613  wemapwe  7618  karden  7783  aceq1  7962  zorn2lem1  8340  axrepndlem2  8432  axregndlem2  8442  pwfseqlem4  8501  gruurn  8637  indpi  8748  nqereu  8770  prcdnq  8834  supexpr  8895  ltsosr  8933  supsrlem  8950  supsr  8951  axpre-lttrn  9005  axpre-sup  9008  prodgt0  9819  infm3  9931  prime  10314  raluz  10489  zsupss  10529  uzsupss  10532  xrsupsslem  10849  xrinfmsslem  10850  fz1sbc  11087  brfi1uzind  11678  wrdind  11754  rexanre  12113  rexico  12120  limsupgle  12234  rlim2lt  12254  rlim3  12255  ello12  12273  ello12r  12274  ello1d  12280  elo12  12284  elo12r  12285  rlimconst  12301  lo1resb  12321  o1resb  12323  rlimcn2  12347  addcn2  12350  mulcn2  12352  reccn2  12353  cn1lem  12354  o1rlimmul  12375  lo1le  12408  caucvgrlem  12429  divrcnv  12595  rpnnen2  12788  sqr2irr  12811  exprmfct  13073  isprm5  13075  prmdvdsexpr  13079  prmpwdvds  13235  vdwmc2  13310  ramtlecl  13331  ramub  13344  rami  13346  ramcl  13360  firest  13623  mreexexd  13836  acsfn  13847  prslem  14351  ispos  14367  posi  14370  isposd  14375  lubval  14399  glbval  14404  joinval2  14409  meetval2  14416  pospropd  14524  spwval2  14619  spwpr2  14623  odlem1  15136  mndodcongi  15144  gexlem1  15176  sylow1lem3  15197  efgredlemb  15341  efgred  15343  frgpnabllem1  15447  isrrg  16311  mplsubglem  16461  mpllsslem  16462  ltbval  16495  opsrval  16498  xrsdsreclb  16708  istopg  16931  isclo2  17115  neiptoptop  17158  neiptopnei  17159  lmbr  17284  ist0  17346  ist1-2  17373  t1sep2  17395  cmpfi  17433  2ndcdisj  17480  1stccn  17487  iskgen3  17542  ptpjopn  17605  hausdiag  17638  xkopt  17648  ist0-4  17722  isr0  17730  r0sep  17741  fbfinnfr  17834  fmfnfmlem2  17948  fmfnfmlem4  17950  fmfnfm  17951  cnflf  17995  cnfcf  18035  tmdgsum2  18087  tsmsgsum  18129  tsmsres  18134  tsmsf1o  18135  tsmsxplem1  18143  tsmsxp  18145  ustssel  18196  ustincl  18198  ustdiag  18199  ustinvel  18200  ustexhalf  18201  ust0  18210  ustuqtop4  18235  utopsnneiplem  18238  isucn2  18270  iducn  18274  metcnp  18532  metcnpi3  18537  txmetcnp  18538  metucnOLD  18579  metucn  18580  ngptgp  18638  nlmvscnlem1  18683  nrginvrcnlem  18687  nghmcn  18740  xrge0tsms  18826  xmetdcn2  18829  metdscn  18847  addcnlem  18855  elcncf1di  18886  ipcnlem1  19160  caucfil  19197  metcld  19219  metcld2  19220  volcn  19459  itg2cnlem2  19615  ellimc2  19725  dveflem  19824  dvne0  19856  mdegleb  19948  mdegle0  19961  ply1divex  20020  fta1g  20051  dgrco  20154  plydivex  20175  fta1  20186  vieta1  20190  abelthlem8  20316  divlogrlim  20487  cxpcn3lem  20592  rlimcnp  20765  cxplim  20771  cxploglim  20777  ftalem1  20816  ftalem2  20817  dvdsmulf1o  20940  ppiublem1  20947  dchrinv  21006  lgseisenlem2  21095  2sqlem6  21114  2sqlem8  21117  2sqlem10  21119  dchrisum0  21175  3v3e3cycl1  21592  constr3trllem2  21599  4cycl4v4e  21614  4cycl4dv4e  21616  eupatrl  21651  rngoidmlem  21972  isnvlem  22050  vacn  22151  nmcvcn  22152  smcnlem  22154  blocni  22267  norm3lemt  22615  isch2  22687  chlimi  22698  omlsii  22866  eigorth  23302  0cnop  23443  0cnfn  23444  idcnop  23445  lnconi  23497  stcltr1i  23738  elat2  23804  funcnv5mpt  24045  resspos  24148  xrge0tsmsd  24184  qqhcn  24336  qqhucn  24337  erdszelem8  24845  ghomf1olem  25066  climuzcnv  25069  relexpindlem  25100  relexpind  25101  rtrclreclem.trans  25107  rtrclind  25110  poseq  25475  frrlem4  25506  nocvxminlem  25566  elfuns  25676  axlowdimlem15  25807  ifscgr  25890  idinside  25930  brsegle  25954  mbfresfi  26160  itg2addnc  26166  trer  26217  filnetlem4  26308  filbcmb  26340  sdclem2  26344  fdc  26347  fdc1  26348  divrngidl  26536  pridlval  26541  smprngopr  26560  ralxpxfr2d  26639  aomclem8  27035  islindf4  27184  hbtlem5  27208  acsfn1p  27383  2sbc6g  27491  sbiota1  27510  wallispilem3  27691  swrdccatin2  28026  swrdccat3b  28039  usgra2pthspth  28043  usgra2wlkspthlem1  28044  usgra2wlkspthlem2  28045  usgra2pthlem1  28048  frgrawopreglem2  28156  usg2spot2nb  28176  bnj1145  29080  bnj1171  29087  bnj1172  29088  drsb1NEW7  29224  ax11v2NEW7  29246  isat3  29802  iscvlat2N  29819  psubspset  30238  ldilfset  30602  ldilset  30603  dilfsetN  30646  dilsetN  30647  cdlemefrs29bpre0  30890  cdlemefrs29clN  30893  cdlemefrs32fva  30894  cdlemn11pre  31705  dihord2pre  31720  lpolsetN  31977
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