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

Theorem orbi1d 746
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
orbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
orbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem orbi1d
StepHypRef Expression
1 orbid.1 . . 3 (𝜑 → (𝜓𝜒))
21orbi2d 745 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 688 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 688 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 222 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wo 670
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1  747  orbi12d  748  xorbi1d  1327  eueq2dc  2810  uneq1  3170  r19.45mv  3403  rexprg  3522  rextpg  3524  swopolem  4165  sowlin  4180  onsucelsucexmidlem1  4381  onsucelsucexmid  4383  ordsoexmid  4415  isosolem  5657  acexmidlema  5697  acexmidlemb  5698  acexmidlem2  5703  acexmidlemv  5704  freceq1  6219  elinp  7183  prloc  7200  ltsosr  7460  axpre-ltwlin  7568  apreap  8215  apreim  8231  sup3exmid  8573  nn01to3  9259  ltxr  9403  fzpr  9698  elfzp12  9720  lcmval  11537  lcmass  11559  isprm6  11618
  Copyright terms: Public domain W3C validator