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

Theorem orbi1d 792
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 791 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 729 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 729 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 223 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wo 709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orbi1  793  orbi12d  794  xorbi1d  1392  eueq2dc  2925  uneq1  3297  r19.45mv  3531  rexprg  3659  rextpg  3661  swopolem  4323  sowlin  4338  onsucelsucexmidlem1  4545  onsucelsucexmid  4547  ordsoexmid  4579  isosolem  5845  acexmidlema  5886  acexmidlemb  5887  acexmidlem2  5892  acexmidlemv  5893  freceq1  6416  exmidaclem  7236  exmidac  7237  elinp  7502  prloc  7519  suplocexprlemloc  7749  ltsosr  7792  suplocsrlemb  7834  axpre-ltwlin  7911  axpre-suploclemres  7929  axpre-suploc  7930  apreap  8573  apreim  8589  sup3exmid  8943  nn01to3  9646  ltxr  9804  fzpr  10106  elfzp12  10128  lcmval  12094  lcmass  12116  isprm6  12178  lringuplu  13540  dedekindeulemloc  14549  dedekindeulemeu  14552  suplociccreex  14554  dedekindicclemloc  14558  dedekindicclemeu  14561
  Copyright terms: Public domain W3C validator