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  526  imordc  780  drsb1  1656  ax11v2  1677  ax11v  1684  ax11ev  1685  equs5or  1687  raleqf  2473  alexeq  2641  mo2icl  2691  sbc19.21g  2797  csbiebg  2860  ralss  2977  ssuni  3568  intmin4  3609  ssexg  3862  pocl  4006  elirr  4199  en2lp  4207  tfisi  4228  vtoclr  4306  sosng  4331  fun11  4883  funimass4  5140  dff13  5323  f1mpt  5326  isopolem  5377  oprabid  5452  caovcan  5579  caoftrn  5650  dfsmo2  5815  qliftfun  6090  ecoptocl  6095  ecopovtrn  6105  ecopovtrng  6108  ltsonq  6246  prarloclem3  6340  lttrsr  6503  mulextsr1  6520  axpre-lttrn  6576  axpre-mulext  6580  prime  7905  bj-rspgt  8382  bdssexg  8477
  Copyright terms: Public domain W3C validator