ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d GIF version

Theorem imbi1d 230
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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimprd 157 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 75 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 143 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 75 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 128 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  583  imordc  867  drsb1  1755  ax11v2  1776  ax11v  1783  ax11ev  1784  equs5or  1786  raleqf  2599  rspceaimv  2771  alexeq  2785  mo2icl  2836  sbc19.21g  2949  csbiebg  3012  ralss  3133  ifmdc  3479  ssuni  3728  intmin4  3769  ssexg  4037  pocl  4195  frforeq1  4235  frforeq2  4237  frind  4244  ontr2exmid  4410  elirr  4426  en2lp  4439  tfisi  4471  vtoclr  4557  sosng  4582  fun11  5160  funimass4  5440  dff13  5637  f1mpt  5640  isopolem  5691  oprabid  5771  caovcan  5903  caoftrn  5975  dfsmo2  6152  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemres  6227  tfrcl  6229  qliftfun  6479  ecoptocl  6484  ecopovtrn  6494  ecopovtrng  6497  dom2lem  6634  ssfiexmid  6738  domfiexmid  6740  findcard  6750  findcard2  6751  findcard2s  6752  fiintim  6785  supmoti  6848  eqsupti  6851  suplubti  6855  supisoex  6864  isomnimap  6977  ismkvmap  6996  ltsonq  7174  prarloclem3  7273  suplocexpr  7501  lttrsr  7538  mulextsr1  7557  suplocsrlem  7584  axpre-lttrn  7660  axpre-mulext  7664  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  prime  9118  raluz  9341  indstr  9356  supinfneg  9358  infsupneg  9359  fz1sbc  9844  exbtwnzlemshrink  9994  rebtwn2zlemshrink  9999  zfz1iso  10552  caucvgre  10721  maxleast  10953  rexanre  10960  rexico  10961  minmax  10969  xrminmax  11002  addcn2  11047  mulcn2  11049  cn1lem  11051  zsupcllemstep  11565  zsupcllemex  11566  bezoutlemmain  11613  dfgcd2  11629  exprmfct  11745  prmdvdsexpr  11755  sqrt2irr  11767  pw2dvdslemn  11770  istopg  12093  lmbr  12309  metcnp  12608  addcncntoplem  12647  bj-rspgt  12920  bdssexg  13029
  Copyright terms: Public domain W3C validator