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

Theorem orbi1d 786
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 785 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 723 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 723 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 222 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wo 703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1  787  orbi12d  788  xorbi1d  1376  eueq2dc  2903  uneq1  3274  r19.45mv  3508  rexprg  3635  rextpg  3637  swopolem  4290  sowlin  4305  onsucelsucexmidlem1  4512  onsucelsucexmid  4514  ordsoexmid  4546  isosolem  5803  acexmidlema  5844  acexmidlemb  5845  acexmidlem2  5850  acexmidlemv  5851  freceq1  6371  exmidaclem  7185  exmidac  7186  elinp  7436  prloc  7453  suplocexprlemloc  7683  ltsosr  7726  suplocsrlemb  7768  axpre-ltwlin  7845  axpre-suploclemres  7863  axpre-suploc  7864  apreap  8506  apreim  8522  sup3exmid  8873  nn01to3  9576  ltxr  9732  fzpr  10033  elfzp12  10055  lcmval  12017  lcmass  12039  isprm6  12101  dedekindeulemloc  13391  dedekindeulemeu  13394  suplociccreex  13396  dedekindicclemloc  13400  dedekindicclemeu  13403
  Copyright terms: Public domain W3C validator