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

Theorem orbi1d 780
 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 779 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 717 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 717 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 222 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 697 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 698 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  orbi1  781  orbi12d  782  xorbi1d  1359  eueq2dc  2857  uneq1  3223  r19.45mv  3456  rexprg  3575  rextpg  3577  swopolem  4227  sowlin  4242  onsucelsucexmidlem1  4443  onsucelsucexmid  4445  ordsoexmid  4477  isosolem  5725  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  acexmidlemv  5772  freceq1  6289  exmidaclem  7069  exmidac  7070  elinp  7294  prloc  7311  suplocexprlemloc  7541  ltsosr  7584  suplocsrlemb  7626  axpre-ltwlin  7703  axpre-suploclemres  7721  axpre-suploc  7722  apreap  8361  apreim  8377  sup3exmid  8727  nn01to3  9421  ltxr  9574  fzpr  9869  elfzp12  9891  lcmval  11755  lcmass  11777  isprm6  11836  dedekindeulemloc  12780  dedekindeulemeu  12783  suplociccreex  12785  dedekindicclemloc  12789  dedekindicclemeu  12792
 Copyright terms: Public domain W3C validator