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

Theorem orbi1d 692
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 691 . 2 (φ → ((θ ψ) ↔ (θ χ)))
3 orcom 634 . 2 ((ψ θ) ↔ (θ ψ))
4 orcom 634 . 2 ((χ θ) ↔ (θ χ))
52, 3, 43bitr4g 212 1 (φ → ((ψ θ) ↔ (χ θ)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   wo 616
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 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orbi1  693  orbi12d  694  xorbi1d  1256  eueq2dc  2691  uneq1  3067  r19.45mv  3294  rexprg  3396  rextpg  3398  swopolem  4016  sowlin  4031  onsucelsucexmidlem1  4197  onsucelsucexmid  4199  ordsoexmid  4224  isosolem  5388  acexmidlema  5427  acexmidlemb  5428  acexmidlem2  5433  acexmidlemv  5434  elinp  6328  prloc  6345  ltsosr  6511  axpre-ltwlin  6577
  Copyright terms: Public domain W3C validator