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

Theorem orbi2i 757
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 756 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 132 . . 3 (𝜓𝜑)
54orim2i 756 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 125 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1i  758  orbi12i  759  orass  762  or4  766  or42  767  orordir  769  dcnnOLD  844  orbididc  948  3orcomb  982  excxor  1373  xordc  1387  nf4dc  1663  nf4r  1664  19.44  1675  dveeq2  1808  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  dcne  2351  unass  3284  undi  3375  undif3ss  3388  symdifxor  3393  undif4  3477  iinuniss  3955  ordsucim  4484  suc11g  4541  qfto  5000  nntri3or  6472  reapcotr  8517  elnn0  9137  elxnn0  9200  elnn1uz2  9566  nn01to3  9576  elxr  9733  xaddcom  9818  xnegdi  9825  xpncan  9828  xleadd1a  9830  lcmdvds  12033  mulgcddvds  12048  cncongr2  12058  pythagtrip  12237  bj-peano4  13990  apdifflemr  14079
  Copyright terms: Public domain W3C validator