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

Theorem orbi2d 703
 Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
orbid.1 (φ → (ψχ))
Assertion
Ref Expression
orbi2d (φ → ((θ ψ) ↔ (θ χ)))

Proof of Theorem orbi2d
StepHypRef Expression
1 orbid.1 . . . 4 (φ → (ψχ))
21biimpd 132 . . 3 (φ → (ψχ))
32orim2d 701 . 2 (φ → ((θ ψ) → (θ χ)))
41biimprd 147 . . 3 (φ → (χψ))
54orim2d 701 . 2 (φ → ((θ χ) → (θ ψ)))
63, 5impbid 120 1 (φ → ((θ ψ) ↔ (θ χ)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98   ∨ wo 628 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  orbi1d  704  orbi12d  706  dn1dc  866  xorbi2d  1269  eueq2dc  2708  rexprg  3413  rextpg  3415  swopolem  4033  sowlin  4048  elsucg  4107  elsuc2g  4108  ordsoexmid  4240  poleloe  4667  isosolem  5406  freceq2  5920  brdifun  6069  pitric  6305  elinp  6457  prloc  6474  ltexprlemloc  6581  ltsosr  6692  aptisr  6705  axpre-ltwlin  6767  gt0add  7357  apreap  7371  apreim  7387  elznn0  8036  elznn  8037  peano2z  8057  zindd  8132  elfzp1  8704  fzm1  8732  fzosplitsni  8861  cjap  9134  bj-nn0sucALT  9438
 Copyright terms: Public domain W3C validator