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

Theorem orbi1d 715
 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 714 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 657 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 657 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 216 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102   ∨ wo 639 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  orbi1  716  orbi12d  717  xorbi1d  1288  eueq2dc  2736  uneq1  3117  r19.45mv  3342  rexprg  3449  rextpg  3451  swopolem  4069  sowlin  4084  onsucelsucexmidlem1  4280  onsucelsucexmid  4282  ordsoexmid  4313  isosolem  5490  acexmidlema  5530  acexmidlemb  5531  acexmidlem2  5536  acexmidlemv  5537  freceq1  6009  elinp  6629  prloc  6646  ltsosr  6906  axpre-ltwlin  7014  apreap  7651  apreim  7667  nn01to3  8648  ltxr  8795  fzpr  9040  elfzp12  9062
 Copyright terms: Public domain W3C validator