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

Theorem orbi2i 679
 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 678 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 124 . . 3 (𝜓𝜑)
54orim2i 678 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 117 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   ∨ wo 629 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 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  orbi1i  680  orbi12i  681  orass  684  or4  688  or42  689  orordir  691  testbitestn  823  orbididc  860  3orcomb  894  excxor  1269  xordc  1283  nf4dc  1560  nf4r  1561  19.44  1572  dveeq2  1696  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  dcne  2216  unass  3100  undi  3185  undif3ss  3198  symdifxor  3203  undif4  3284  iinuniss  3737  ordsucim  4226  suc11g  4281  qfto  4714  nntri3or  6072  reapcotr  7589  elnn0  8183  elnn1uz2  8544  nn01to3  8552  elxr  8696  bj-peano4  10080
 Copyright terms: Public domain W3C validator