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

Theorem orbi1d 704
 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 703 . 2 (φ → ((θ ψ) ↔ (θ χ)))
3 orcom 646 . 2 ((ψ θ) ↔ (θ ψ))
4 orcom 646 . 2 ((χ θ) ↔ (θ χ))
52, 3, 43bitr4g 212 1 (φ → ((ψ θ) ↔ (χ θ)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98   ∨ wo 628 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  orbi1  705  orbi12d  706  xorbi1d  1270  eueq2dc  2708  uneq1  3084  r19.45mv  3309  rexprg  3413  rextpg  3415  swopolem  4033  sowlin  4048  onsucelsucexmidlem1  4213  onsucelsucexmid  4215  ordsoexmid  4240  isosolem  5406  acexmidlema  5446  acexmidlemb  5447  acexmidlem2  5452  acexmidlemv  5453  freceq1  5919  elinp  6456  prloc  6473  ltsosr  6672  axpre-ltwlin  6747  apreap  7351  apreim  7367  nn01to3  8308  ltxr  8445  fzpr  8689  elfzp12  8711
 Copyright terms: Public domain W3C validator