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

Theorem orim12d 700
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 699 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ta ) )  ->  (
( ps  \/  th )  ->  ( ch  \/  ta ) ) )
41, 2, 3syl2anc 391 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1d  701  orim2d  702  3orim123d  1215  19.33b2  1520  preq12b  3541  prel12  3542  funun  4944  nnsucelsuc  6070  nnaord  6082  nnmord  6090  swoer  6134  fidceq  6330  fin0or  6343  ltsopr  6694  cauappcvgprlemloc  6750  caucvgprlemloc  6773  caucvgprprlemloc  6801  mulextsr1lem  6864  reapcotr  7589  apcotr  7598  mulext1  7603  mulext  7605  peano2z  8281  zeo  8343  uzm1  8503  eluzdc  8547  fzospliti  9032  frec2uzltd  9189  absext  9661  bj-findis  10104
  Copyright terms: Public domain W3C validator