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  3476  iinuniss  3953  ordsucim  4482  suc11g  4539  qfto  4998  nntri3or  6469  reapcotr  8504  elnn0  9124  elxnn0  9187  elnn1uz2  9553  nn01to3  9563  elxr  9720  xaddcom  9805  xnegdi  9812  xpncan  9815  xleadd1a  9817  lcmdvds  12020  mulgcddvds  12035  cncongr2  12045  pythagtrip  12224  bj-peano4  13912  apdifflemr  14001
  Copyright terms: Public domain W3C validator