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

Theorem orbi2d 790
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 144 . . 3 (𝜑 → (𝜓𝜒))
32orim2d 788 . 2 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
41biimprd 158 . . 3 (𝜑 → (𝜒𝜓))
54orim2d 788 . 2 (𝜑 → ((𝜃𝜒) → (𝜃𝜓)))
63, 5impbid 129 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  orbi1d  791  orbi12d  793  dn1dc  960  xorbi2d  1380  eueq2dc  2910  r19.44mv  3517  rexprg  3643  rextpg  3645  exmidsssn  4199  exmidsssnc  4200  swopolem  4301  sowlin  4316  elsucg  4400  elsuc2g  4401  ordsoexmid  4557  poleloe  5023  isosolem  5818  freceq2  6387  brdifun  6555  pitric  7298  elinp  7451  prloc  7468  ltexprlemloc  7584  suplocexprlemloc  7698  ltsosr  7741  aptisr  7756  suplocsrlemb  7783  axpre-ltwlin  7860  axpre-suploclemres  7878  axpre-suploc  7879  gt0add  8507  apreap  8521  apreim  8537  elznn0  9244  elznn  9245  peano2z  9265  zindd  9347  elfzp1  10045  fzm1  10073  fzosplitsni  10208  cjap  10886  dvdslelemd  11819  zeo5  11863  lcmval  12033  lcmneg  12044  lcmass  12055  isprm6  12117  infpn2  12427  dedekindeulemloc  13730  dedekindeulemeu  13733  suplociccreex  13735  dedekindicclemloc  13739  dedekindicclemeu  13742  bj-charfunr  14184  bj-nn0sucALT  14352
  Copyright terms: Public domain W3C validator