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

Theorem orbi1d 738
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 737 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 680 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 680 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 221 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:  orbi1  739  orbi12d  740  xorbi1d  1315  eueq2dc  2779  uneq1  3136  r19.45mv  3362  rexprg  3477  rextpg  3479  swopolem  4105  sowlin  4120  onsucelsucexmidlem1  4316  onsucelsucexmid  4318  ordsoexmid  4350  isosolem  5558  acexmidlema  5598  acexmidlemb  5599  acexmidlem2  5604  acexmidlemv  5605  freceq1  6105  elinp  6970  prloc  6987  ltsosr  7247  axpre-ltwlin  7355  apreap  7998  apreim  8014  nn01to3  9027  ltxr  9171  fzpr  9414  elfzp12  9436  lcmval  10912  lcmass  10934  isprm6  10993
  Copyright terms: Public domain W3C validator