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

Theorem orim2d 760
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
Ref Expression
orim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
orim2d  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )

Proof of Theorem orim2d
StepHypRef Expression
1 idd 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2orim12d 758 1  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ 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:  orim2  761  orbi2d  762  pm2.82  784  stdcndcOLD  814  pm2.13dc  853  exmid1dc  4091  acexmidlemcase  5735  poxp  6095  fodjuomnilemdc  6982  indpi  7114  suplocexprlemloc  7493  nneoor  9104  uzp1  9308  maxabslemlub  10919  xrmaxiflemlub  10957  exmidunben  11834  bj-nn0suc  12964  sbthomlem  13022
  Copyright terms: Public domain W3C validator