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

Theorem orbi2i 763
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 120 . . 3 (𝜑𝜓)
32orim2i 762 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 133 . . 3 (𝜓𝜑)
54orim2i 762 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 126 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wb 105  wo 709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orbi1i  764  orbi12i  765  orass  768  or4  772  or42  773  orordir  775  dcnnOLD  850  orbididc  955  3orcomb  989  excxor  1389  xordc  1403  nf4dc  1681  nf4r  1682  19.44  1693  dveeq2  1826  dvelimALT  2022  dvelimfv  2023  dvelimor  2030  dcne  2371  unass  3307  undi  3398  undif3ss  3411  symdifxor  3416  undif4  3500  iinuniss  3984  ordsucim  4514  suc11g  4571  qfto  5033  nntri3or  6512  reapcotr  8573  elnn0  9196  elxnn0  9259  elnn1uz2  9625  nn01to3  9635  elxr  9794  xaddcom  9879  xnegdi  9886  xpncan  9889  xleadd1a  9891  lcmdvds  12097  mulgcddvds  12112  cncongr2  12122  pythagtrip  12301  bj-peano4  15104  apdifflemr  15193
  Copyright terms: Public domain W3C validator