ILE Home 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  6652  axpre-ltwlin  6727  apreap  7331  apreim  7347  nn01to3  8288  ltxr  8425  fzpr  8669  elfzp12  8691
  Copyright terms: Public domain W3C validator