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

Theorem imbi1d 224
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 151 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 73 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 136 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 73 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 124 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imbi12d  227  imbi1  229  imim21b  245  pm5.33  551  imordc  807  drsb1  1696  ax11v2  1717  ax11v  1724  ax11ev  1725  equs5or  1727  raleqf  2518  alexeq  2693  mo2icl  2743  sbc19.21g  2854  csbiebg  2917  ralss  3034  ssuni  3630  intmin4  3671  ssexg  3924  pocl  4068  frforeq1  4108  frforeq2  4110  frind  4117  ontr2exmid  4278  elirr  4294  en2lp  4306  tfisi  4338  vtoclr  4416  sosng  4441  fun11  4994  funimass4  5252  dff13  5435  f1mpt  5438  isopolem  5489  oprabid  5565  caovcan  5693  caoftrn  5764  dfsmo2  5933  qliftfun  6219  ecoptocl  6224  ecopovtrn  6234  ecopovtrng  6237  dom2lem  6283  ssfiexmid  6367  findcard  6376  findcard2  6377  findcard2s  6378  supmoti  6399  eqsupti  6402  suplubti  6406  supisoex  6413  ltsonq  6554  prarloclem3  6653  lttrsr  6905  mulextsr1  6923  axpre-lttrn  7016  axpre-mulext  7020  axcaucvglemres  7031  prime  8396  raluz  8617  indstr  8632  fz1sbc  9060  qbtwnzlemshrink  9206  rebtwn2zlemshrink  9210  caucvgre  9808  addcn2  10062  mulcn2  10064  cn1lem  10065  sqrt2irr  10251  pw2dvdslemn  10253  bj-rspgt  10312  bdssexg  10411
  Copyright terms: Public domain W3C validator