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

Theorem orbi2i 720
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 119 . . 3 (𝜑𝜓)
32orim2i 719 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 132 . . 3 (𝜓𝜑)
54orim2i 719 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 125 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 670
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1i  721  orbi12i  722  orass  725  or4  729  or42  730  orordir  732  testbitestn  867  orbididc  905  3orcomb  939  excxor  1324  xordc  1338  nf4dc  1616  nf4r  1617  19.44  1628  dveeq2  1754  dvelimALT  1946  dvelimfv  1947  dvelimor  1954  dcne  2278  unass  3180  undi  3271  undif3ss  3284  symdifxor  3289  undif4  3372  iinuniss  3841  ordsucim  4354  suc11g  4410  qfto  4864  nntri3or  6319  reapcotr  8226  elnn0  8831  elxnn0  8894  elnn1uz2  9251  nn01to3  9259  elxr  9404  xaddcom  9485  xnegdi  9492  xpncan  9495  xleadd1a  9497  lcmdvds  11553  mulgcddvds  11568  cncongr2  11578  bj-peano4  12738
  Copyright terms: Public domain W3C validator