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

Theorem orbi2i 712
 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 118 . . 3 (𝜑𝜓)
32orim2i 711 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 131 . . 3 (𝜓𝜑)
54orim2i 711 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 124 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   ↔ wb 103   ∨ wo 662 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  orbi1i  713  orbi12i  714  orass  717  or4  721  or42  722  orordir  724  testbitestn  857  orbididc  895  3orcomb  929  excxor  1310  xordc  1324  nf4dc  1601  nf4r  1602  19.44  1613  dveeq2  1737  dvelimALT  1928  dvelimfv  1929  dvelimor  1936  dcne  2257  unass  3130  undi  3213  undif3ss  3226  symdifxor  3231  undif4  3307  iinuniss  3760  ordsucim  4246  suc11g  4302  qfto  4738  nntri3or  6130  reapcotr  7754  elnn0  8346  elxnn0  8409  elnn1uz2  8764  nn01to3  8772  elxr  8917  lcmdvds  10594  mulgcddvds  10609  cncongr2  10619  bj-peano4  10893
 Copyright terms: Public domain W3C validator