ILE Home 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  859  orbididc  897  3orcomb  931  excxor  1312  xordc  1326  nf4dc  1603  nf4r  1604  19.44  1615  dveeq2  1740  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  dcne  2262  unass  3146  undi  3236  undif3ss  3249  symdifxor  3254  undif4  3333  iinuniss  3793  ordsucim  4290  suc11g  4346  qfto  4788  nntri3or  6208  reapcotr  8016  elnn0  8608  elxnn0  8671  elnn1uz2  9026  nn01to3  9034  elxr  9179  lcmdvds  10936  mulgcddvds  10951  cncongr2  10961  bj-peano4  11288
  Copyright terms: Public domain W3C validator