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

Theorem imbi1d 220
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 147 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 69 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 132 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 69 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 120 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  imbi12d  223  imbi1  225  imim21b  241  pm5.33  541  imordc  796  drsb1  1680  ax11v2  1701  ax11v  1708  ax11ev  1709  equs5or  1711  raleqf  2501  alexeq  2670  mo2icl  2720  sbc19.21g  2826  csbiebg  2889  ralss  3006  ssuni  3602  intmin4  3643  ssexg  3896  pocl  4040  frforeq1  4080  frforeq2  4082  frind  4089  ontr2exmid  4250  elirr  4266  en2lp  4278  tfisi  4310  vtoclr  4388  sosng  4413  fun11  4966  funimass4  5224  dff13  5407  f1mpt  5410  isopolem  5461  oprabid  5537  caovcan  5665  caoftrn  5736  dfsmo2  5902  qliftfun  6188  ecoptocl  6193  ecopovtrn  6203  ecopovtrng  6206  dom2lem  6252  ssfiexmid  6336  findcard  6345  findcard2  6346  findcard2s  6347  ltsonq  6496  prarloclem3  6595  lttrsr  6847  mulextsr1  6865  axpre-lttrn  6958  axpre-mulext  6962  axcaucvglemres  6973  prime  8337  raluz  8521  indstr  8536  fz1sbc  8958  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  caucvgre  9580  addcn2  9831  mulcn2  9833  cn1lem  9834  sqrt2irr  9878  bj-rspgt  9925  bdssexg  10024
  Copyright terms: Public domain W3C validator