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

Theorem orbi2i 666
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 665 . 2 ((χ φ) → (χ ψ))
41biimpri 124 . . 3 (ψφ)
54orim2i 665 . 2 ((χ ψ) → (χ φ))
63, 5impbii 117 1 ((χ φ) ↔ (χ ψ))
Colors of variables: wff set class
Syntax hints:  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:  orbi1i  667  orbi12i  668  orass  671  or4  675  or42  676  orordir  678  testbitestn  732  orbididc  848  3orcomb  882  excxor  1254  xordc  1266  nf4dc  1542  nf4r  1543  19.44  1554  dveeq2  1678  dvelimALT  1868  dvelimfv  1869  dvelimor  1876  exmidnedc  2195  unass  3077  undi  3162  undif3ss  3175  symdifxor  3180  undif4  3261  iinuniss  3711  ordsucim  4176  suc11g  4219  qfto  4641  nntri3or  5987  bj-peano4  7324
  Copyright terms: Public domain W3C validator