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

Theorem orbi2d 737
 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 142 . . 3 (𝜑 → (𝜓𝜒))
32orim2d 735 . 2 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
41biimprd 156 . . 3 (𝜑 → (𝜒𝜓))
54orim2d 735 . 2 (𝜑 → ((𝜃𝜒) → (𝜃𝜓)))
63, 5impbid 127 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103   ∨ wo 662 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  orbi1d  738  orbi12d  740  dn1dc  902  xorbi2d  1312  eueq2dc  2774  r19.44mv  3352  rexprg  3462  rextpg  3464  swopolem  4088  sowlin  4103  elsucg  4187  elsuc2g  4188  ordsoexmid  4333  poleloe  4774  isosolem  5515  freceq2  6063  brdifun  6221  pitric  6643  elinp  6796  prloc  6813  ltexprlemloc  6929  ltsosr  7073  aptisr  7087  axpre-ltwlin  7181  gt0add  7810  apreap  7824  apreim  7840  elznn0  8517  elznn  8518  peano2z  8538  zindd  8616  elfzp1  9235  fzm1  9263  fzosplitsni  9391  cjap  10012  dvdslelemd  10469  zeo5  10513  lcmval  10670  lcmneg  10681  lcmass  10692  isprm6  10751  bj-nn0sucALT  11058
 Copyright terms: Public domain W3C validator