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

Theorem orbi2i 678
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
Hypothesis
Ref Expression
orbi2i.1 (φψ)
Assertion
Ref Expression
orbi2i ((χ φ) ↔ (χ ψ))

Proof of Theorem orbi2i
StepHypRef Expression
1 orbi2i.1 . . . 4 (φψ)
21biimpi 113 . . 3 (φψ)
32orim2i 677 . 2 ((χ φ) → (χ ψ))
41biimpri 124 . . 3 (ψφ)
54orim2i 677 . 2 ((χ ψ) → (χ φ))
63, 5impbii 117 1 ((χ φ) ↔ (χ ψ))
Colors of variables: wff set class
Syntax hints:  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:  orbi1i  679  orbi12i  680  orass  683  or4  687  or42  688  orordir  690  testbitestn  822  orbididc  859  3orcomb  893  excxor  1268  xordc  1280  nf4dc  1557  nf4r  1558  19.44  1569  dveeq2  1693  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  dcne  2211  unass  3094  undi  3179  undif3ss  3192  symdifxor  3197  undif4  3278  iinuniss  3728  ordsucim  4192  suc11g  4235  qfto  4657  nntri3or  6011  reapcotr  7362  elnn0  7939  elnn1uz2  8300  nn01to3  8308  elxr  8446  bj-peano4  9389
  Copyright terms: Public domain W3C validator