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

Theorem orim12d 710
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
orim12d.1  |-  ( ph  ->  ( ps  ->  ch ) )
orim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
orim12d  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )

Proof of Theorem orim12d
StepHypRef Expression
1 orim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 orim12d.2 . 2  |-  ( ph  ->  ( th  ->  ta ) )
3 pm3.48 709 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ta ) )  ->  (
( ps  \/  th )  ->  ( ch  \/  ta ) ) )
41, 2, 3syl2anc 397 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  orim1d  711  orim2d  712  3orim123d  1226  19.33b2  1536  preq12b  3568  prel12  3569  funun  4971  nnsucelsuc  6100  nnaord  6112  nnmord  6120  swoer  6164  fidceq  6360  fin0or  6373  ltsopr  6751  cauappcvgprlemloc  6807  caucvgprlemloc  6830  caucvgprprlemloc  6858  mulextsr1lem  6921  reapcotr  7662  apcotr  7671  mulext1  7676  mulext  7678  peano2z  8337  zeo  8401  uzm1  8598  eluzdc  8643  fzospliti  9133  frec2uzltd  9352  absext  9889  qabsor  9901  dvdslelemd  10154  odd2np1lem  10182  odd2np1  10183  bj-findis  10470
  Copyright terms: Public domain W3C validator