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

Theorem orbi2i 762
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 761 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 133 . . 3 (𝜓𝜑)
54orim2i 761 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 126 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wb 105  wo 708
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 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orbi1i  763  orbi12i  764  orass  767  or4  771  or42  772  orordir  774  dcnnOLD  849  orbididc  953  3orcomb  987  excxor  1378  xordc  1392  nf4dc  1670  nf4r  1671  19.44  1682  dveeq2  1815  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  dcne  2358  unass  3292  undi  3383  undif3ss  3396  symdifxor  3401  undif4  3485  iinuniss  3969  ordsucim  4499  suc11g  4556  qfto  5018  nntri3or  6493  reapcotr  8554  elnn0  9177  elxnn0  9240  elnn1uz2  9606  nn01to3  9616  elxr  9775  xaddcom  9860  xnegdi  9867  xpncan  9870  xleadd1a  9872  lcmdvds  12078  mulgcddvds  12093  cncongr2  12103  pythagtrip  12282  bj-peano4  14677  apdifflemr  14765
  Copyright terms: Public domain W3C validator