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

Theorem orbi2i 751
 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 750 . 2 ((𝜒𝜑) → (𝜒𝜓))
41biimpri 132 . . 3 (𝜓𝜑)
54orim2i 750 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 125 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   ∨ wo 697 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 698 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  orbi1i  752  orbi12i  753  orass  756  or4  760  or42  761  orordir  763  dcnnOLD  834  orbididc  937  3orcomb  971  excxor  1356  xordc  1370  nf4dc  1648  nf4r  1649  19.44  1660  dveeq2  1787  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  dcne  2319  unass  3233  undi  3324  undif3ss  3337  symdifxor  3342  undif4  3425  iinuniss  3895  ordsucim  4416  suc11g  4472  qfto  4928  nntri3or  6389  reapcotr  8372  elnn0  8991  elxnn0  9054  elnn1uz2  9413  nn01to3  9421  elxr  9575  xaddcom  9656  xnegdi  9663  xpncan  9666  xleadd1a  9668  lcmdvds  11771  mulgcddvds  11786  cncongr2  11796  bj-peano4  13212  apdifflemr  13301
 Copyright terms: Public domain W3C validator