ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d Structured version   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  795  drsb1  1677  ax11v2  1698  ax11v  1705  ax11ev  1706  equs5or  1708  raleqf  2495  alexeq  2664  mo2icl  2714  sbc19.21g  2820  csbiebg  2883  ralss  3000  ssuni  3593  intmin4  3634  ssexg  3887  pocl  4031  elirr  4224  en2lp  4232  tfisi  4253  vtoclr  4331  sosng  4356  fun11  4909  funimass4  5167  dff13  5350  f1mpt  5353  isopolem  5404  oprabid  5480  caovcan  5607  caoftrn  5678  dfsmo2  5843  qliftfun  6124  ecoptocl  6129  ecopovtrn  6139  ecopovtrng  6142  dom2lem  6188  ssfiexmid  6254  ltsonq  6382  prarloclem3  6479  lttrsr  6670  mulextsr1  6687  axpre-lttrn  6748  axpre-mulext  6752  prime  8093  raluz  8277  indstr  8292  fz1sbc  8708  bj-rspgt  9240  bdssexg  9335
  Copyright terms: Public domain W3C validator