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  873  con3th  949  19.21t  1838  ax12v2  2033  drsb1  2068  ax12vALT  2131  ax12inda  2249  ax12v2-o  2250  ralcom2  2906  raleqf  2934  ralxpxfr2d  3105  alexeqg  3109  alexeq  3110  mo2icl  3159  sbc19.21g  3280  csbiebg  3332  ralss  3439  r19.37zv  3797  ssuni  4134  intmin4  4178  ssexg  4459  pocl  4669  vtoclr  4904  frsn  4930  fun11  5504  funimass4  5763  dff13  5992  f1mpt  5995  isopolem  6057  oprabid  6136  caovcan  6288  caoftrn  6376  ordunisuc2  6476  tfisi  6490  tfinds  6491  tfindsg  6492  tfindsg2  6493  dfom2  6499  findsg  6524  frxp  6703  dfsmo2  6829  qliftfun  7206  ecoptocl  7211  ecopovtrn  7224  dom2lem  7370  findcard  7572  findcard2  7573  findcard3  7576  fiint  7609  supmo  7723  eqsup  7727  suplub  7731  supmaxlem  7735  supisoex  7742  wemaplem1  7781  wemaplem2  7782  wemapsolem  7785  oemapvali  7913  cantnf  7922  cantnfOLD  7944  wemapwe  7949  wemapweOLD  7950  karden  8123  aceq1  8308  zorn2lem1  8686  axrepndlem2  8778  axregndlem2  8790  pwfseqlem4  8850  gruurn  8986  indpi  9097  nqereu  9119  prcdnq  9183  supexpr  9244  ltsosr  9282  supsrlem  9299  supsr  9300  axpre-lttrn  9354  axpre-sup  9357  prodgt0  10195  infm3  10310  prime  10743  raluz  10924  zsupss  10965  uzsupss  10968  xrsupsslem  11290  xrinfmsslem  11291  fz1sbc  11557  brfi1uzind  12240  wrdind  12392  wrd2ind  12393  rexanre  12855  rexico  12862  limsupgle  12976  rlim2lt  12996  rlim3  12997  ello12  13015  ello12r  13016  ello1d  13022  elo12  13026  elo12r  13027  rlimconst  13043  lo1resb  13063  o1resb  13065  rlimcn2  13089  addcn2  13092  mulcn2  13094  reccn2  13095  cn1lem  13096  o1rlimmul  13117  lo1le  13150  caucvgrlem  13171  divrcnv  13336  rpnnen2  13529  sqr2irr  13552  exprmfct  13817  isprm5  13819  prmdvdsexpr  13823  prmpwdvds  13986  vdwmc2  14061  ramtlecl  14082  ramub  14095  rami  14097  ramcl  14111  firest  14392  mreexexd  14607  acsfn  14618  prslem  15122  ispos  15138  posi  15141  isposd  15146  lubeldm  15172  lubval  15175  glbeldm  15185  glbval  15188  joinval2lem  15199  meetval2lem  15213  pospropd  15325  odlem1  16059  mndodcongi  16067  gexlem1  16099  sylow1lem3  16120  efgredlemb  16264  efgred  16266  frgpnabllem1  16372  isrrg  17381  mplsubglem  17532  mpllsslem  17533  mplsubglemOLD  17534  mpllsslemOLD  17535  ltbval  17575  opsrval  17578  xrsdsreclb  17882  islindf4  18289  mdetunilem1  18440  mdetunilem3  18442  mdetunilem4  18443  mdetunilem9  18448  istopg  18530  isclo2  18714  neiptoptop  18757  neiptopnei  18758  lmbr  18884  ist0  18946  ist1-2  18973  t1sep2  18995  cmpfi  19033  2ndcdisj  19082  1stccn  19089  iskgen3  19144  ptpjopn  19207  hausdiag  19240  xkopt  19250  ist0-4  19324  isr0  19332  r0sep  19343  fbfinnfr  19436  fmfnfmlem2  19550  fmfnfmlem4  19552  fmfnfm  19553  cnflf  19597  cnfcf  19637  tmdgsum2  19689  tsmsgsum  19731  tsmsgsumOLD  19734  tsmsresOLD  19739  tsmsres  19740  tsmsf1o  19741  tsmsxplem1  19749  tsmsxp  19751  ustssel  19802  ustincl  19804  ustdiag  19805  ustinvel  19806  ustexhalf  19807  ust0  19816  ustuqtop4  19841  utopsnneiplem  19844  isucn2  19876  iducn  19880  metcnp  20138  metcnpi3  20143  txmetcnp  20144  metucnOLD  20185  metucn  20186  ngptgp  20244  nlmvscnlem1  20289  nrginvrcnlem  20293  nghmcn  20346  xrge0tsms  20433  xmetdcn2  20436  metdscn  20454  addcnlem  20462  elcncf1di  20493  ipcnlem1  20779  caucfil  20816  metcld  20838  metcld2  20839  volcn  21108  itg2cnlem2  21262  ellimc2  21374  dveflem  21473  dvne0  21505  mdegleb  21557  mdegle0  21570  ply1divex  21630  fta1g  21661  dgrco  21764  plydivex  21785  fta1  21796  vieta1  21800  abelthlem8  21926  divlogrlim  22102  cxpcn3lem  22207  rlimcnp  22381  cxplim  22387  cxploglim  22393  ftalem1  22432  ftalem2  22433  dvdsmulf1o  22556  ppiublem1  22563  dchrinv  22622  lgseisenlem2  22711  2sqlem6  22730  2sqlem8  22733  2sqlem10  22735  dchrisum0  22791  istrkgc  22939  istrkgb  22940  axtgcgrid  22946  axtg5seg  22948  axtgpasch  22950  axtgupdim2  22954  axtgeucl  22955  axlowdimlem15  23224  3v3e3cycl1  23552  constr3trllem2  23559  4cycl4v4e  23574  4cycl4dv4e  23576  eupatrl  23611  rngoidmlem  23932  isnvlem  24010  vacn  24111  nmcvcn  24112  smcnlem  24114  blocni  24227  norm3lemt  24576  isch2  24648  chlimi  24659  omlsii  24828  eigorth  25264  0cnop  25405  0cnfn  25406  idcnop  25407  lnconi  25459  stcltr1i  25700  elat2  25766  funcnv5mpt  26010  xrge0infss  26075  resspos  26142  xrge0tsmsd  26275  rngurd  26278  qqhcn  26442  qqhucn  26443  eulerpartlemgvv  26781  sgn3da  26946  sgnnbi  26950  sgnpbi  26951  erdszelem8  27108  ghomf1olem  27335  climuzcnv  27338  relexpindlem  27363  relexpind  27364  rtrclreclem.trans  27370  rtrclind  27373  poseq  27736  frrlem4  27793  nocvxminlem  27853  ifscgr  28097  idinside  28137  brsegle  28161  wl-sbrimt  28400  fin2so  28442  heicant  28452  mbfresfi  28464  itg2addnc  28472  ftc1anc  28501  trer  28537  filnetlem4  28628  filbcmb  28660  sdclem2  28664  fdc  28667  fdc1  28668  divrngidl  28854  pridlval  28859  smprngopr  28878  aomclem8  29440  hbtlem5  29510  acsfn1p  29582  2sbc6g  29695  sbiota1  29714  wallispilem3  29888  ccats1rev  30286  usgra2pthspth  30321  usgra2wlkspthlem1  30322  usgra2wlkspthlem2  30323  usgra2pthlem1  30326  frgrawopreglem2  30664  usg2spot2nb  30684  friendshipgt3  30740  ssnn0fi  30775  ply1mulgsumlem1  30877  ply1mulgsumlem2  30878  bnj1145  32080  bnj1171  32087  bnj1172  32088  bj-con3ALT  32194  bj-axc15v  32361  bj-19.21t  32434  isat3  33048  iscvlat2N  33065  psubspset  33484  ldilfset  33848  ldilset  33849  dilfsetN  33892  dilsetN  33893  cdlemefrs29bpre0  34136  cdlemefrs29clN  34139  cdlemefrs32fva  34140  cdlemn11pre  34951  dihord2pre  34966  lpolsetN  35223
  Copyright terms: Public domain W3C validator