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

Theorem orbi2d 780
 Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
orbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
orbi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem orbi2d
StepHypRef Expression
1 orbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimpd 143 . . 3 (𝜑 → (𝜓𝜒))
32orim2d 778 . 2 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
41biimprd 157 . . 3 (𝜑 → (𝜒𝜓))
54orim2d 778 . 2 (𝜑 → ((𝜃𝜒) → (𝜃𝜓)))
63, 5impbid 128 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 698 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 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  orbi1d  781  orbi12d  783  dn1dc  945  xorbi2d  1359  eueq2dc  2863  r19.44mv  3464  rexprg  3585  rextpg  3587  exmidsssn  4136  exmidsssnc  4137  swopolem  4238  sowlin  4253  elsucg  4337  elsuc2g  4338  ordsoexmid  4488  poleloe  4950  isosolem  5737  freceq2  6302  brdifun  6468  pitric  7182  elinp  7335  prloc  7352  ltexprlemloc  7468  suplocexprlemloc  7582  ltsosr  7625  aptisr  7640  suplocsrlemb  7667  axpre-ltwlin  7744  axpre-suploclemres  7762  axpre-suploc  7763  gt0add  8388  apreap  8402  apreim  8418  elznn0  9122  elznn  9123  peano2z  9143  zindd  9222  elfzp1  9912  fzm1  9940  fzosplitsni  10072  cjap  10739  dvdslelemd  11613  zeo5  11657  lcmval  11816  lcmneg  11827  lcmass  11838  isprm6  11897  dedekindeulemloc  12841  dedekindeulemeu  12844  suplociccreex  12846  dedekindicclemloc  12850  dedekindicclemeu  12853  bj-charfunr  13224  bj-nn0sucALT  13392
 Copyright terms: Public domain W3C validator