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

Theorem orbi2d 714
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 136 . . 3 (𝜑 → (𝜓𝜒))
32orim2d 712 . 2 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
41biimprd 151 . . 3 (𝜑 → (𝜒𝜓))
54orim2d 712 . 2 (𝜑 → ((𝜃𝜒) → (𝜃𝜓)))
63, 5impbid 124 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  orbi1d  715  orbi12d  717  dn1dc  878  xorbi2d  1287  eueq2dc  2736  rexprg  3449  rextpg  3451  swopolem  4069  sowlin  4084  elsucg  4168  elsuc2g  4169  ordsoexmid  4313  poleloe  4751  isosolem  5490  freceq2  6010  brdifun  6163  pitric  6476  elinp  6629  prloc  6646  ltexprlemloc  6762  ltsosr  6906  aptisr  6920  axpre-ltwlin  7014  gt0add  7637  apreap  7651  apreim  7667  elznn0  8316  elznn  8317  peano2z  8337  zindd  8414  elfzp1  9035  fzm1  9063  fzosplitsni  9192  cjap  9733  dvdslelemd  10154  zeo5  10199  bj-nn0sucALT  10469
  Copyright terms: Public domain W3C validator