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

Theorem orbi2d 688
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 686 . 2 (φ → ((θ ψ) → (θ χ)))
41biimprd 147 . . 3 (φ → (χψ))
54orim2d 686 . 2 (φ → ((θ χ) → (θ ψ)))
63, 5impbid 120 1 (φ → ((θ ψ) ↔ (θ χ)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   wo 613
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 614
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orbi1d  689  orbi12d  691  dn1dc  849  xorbi2d  1250  eueq2dc  2682  rexprg  3385  rextpg  3387  swopolem  4005  sowlin  4020  elsucg  4079  elsuc2g  4080  ordsoexmid  4212  poleloe  4639  isosolem  5376  brdifun  6032  pitric  6167  elinp  6314  prloc  6331  ltexprlemloc  6430  ltsosr  6502  aptisr  6515  axpre-ltwlin  6572  gt0add  7160  apreap  7174  apreim  7190  elznn0  7834  elznn  7835  peano2z  7854  zindd  7920  bj-nn0sucALT  8358
  Copyright terms: Public domain W3C validator