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

Theorem orbi2d 737
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 142 . . 3 (𝜑 → (𝜓𝜒))
32orim2d 735 . 2 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
41biimprd 156 . . 3 (𝜑 → (𝜒𝜓))
54orim2d 735 . 2 (𝜑 → ((𝜃𝜒) → (𝜃𝜓)))
63, 5impbid 127 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  orbi1d  738  orbi12d  740  dn1dc  904  xorbi2d  1314  eueq2dc  2779  r19.44mv  3363  rexprg  3477  rextpg  3479  swopolem  4106  sowlin  4121  elsucg  4205  elsuc2g  4206  ordsoexmid  4351  poleloe  4798  isosolem  5564  freceq2  6112  brdifun  6271  pitric  6824  elinp  6977  prloc  6994  ltexprlemloc  7110  ltsosr  7254  aptisr  7268  axpre-ltwlin  7362  gt0add  7991  apreap  8005  apreim  8021  elznn0  8698  elznn  8699  peano2z  8719  zindd  8797  elfzp1  9416  fzm1  9444  fzosplitsni  9574  cjap  10235  dvdslelemd  10719  zeo5  10763  lcmval  10920  lcmneg  10931  lcmass  10942  isprm6  11001  bj-nn0sucALT  11311
  Copyright terms: Public domain W3C validator