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

Theorem orbi2d 762
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 760 . 2 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
41biimprd 157 . . 3 (𝜑 → (𝜒𝜓))
54orim2d 760 . 2 (𝜑 → ((𝜃𝜒) → (𝜃𝜓)))
63, 5impbid 128 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1d  763  orbi12d  765  dn1dc  927  xorbi2d  1341  eueq2dc  2828  r19.44mv  3425  rexprg  3543  rextpg  3545  exmidsssn  4093  exmidsssnc  4094  swopolem  4195  sowlin  4210  elsucg  4294  elsuc2g  4295  ordsoexmid  4445  poleloe  4906  isosolem  5691  freceq2  6256  brdifun  6422  pitric  7093  elinp  7246  prloc  7263  ltexprlemloc  7379  suplocexprlemloc  7493  ltsosr  7536  aptisr  7551  suplocsrlemb  7578  axpre-ltwlin  7655  axpre-suploclemres  7673  axpre-suploc  7674  gt0add  8298  apreap  8312  apreim  8328  elznn0  9020  elznn  9021  peano2z  9041  zindd  9120  elfzp1  9792  fzm1  9820  fzosplitsni  9952  cjap  10618  dvdslelemd  11437  zeo5  11481  lcmval  11640  lcmneg  11651  lcmass  11662  isprm6  11721  dedekindeulemloc  12661  dedekindeulemeu  12664  bj-nn0sucALT  12978
  Copyright terms: Public domain W3C validator