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

Theorem orim12d 735
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 734 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ta ) )  ->  (
( ps  \/  th )  ->  ( ch  \/  ta ) ) )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  orim1d  736  orim2d  737  3orim123d  1256  19.33b2  1565  eqifdc  3425  preq12b  3614  prel12  3615  funun  5058  nnsucelsuc  6252  nnaord  6268  nnmord  6276  swoer  6320  fidceq  6585  fin0or  6602  enomnilem  6794  exmidomni  6798  fodjuomnilemres  6803  ltsopr  7155  cauappcvgprlemloc  7211  caucvgprlemloc  7234  caucvgprprlemloc  7262  mulextsr1lem  7325  reapcotr  8075  apcotr  8084  mulext1  8089  mulext  8091  peano2z  8786  zeo  8851  uzm1  9049  eluzdc  9097  fzospliti  9587  frec2uzltd  9810  absext  10496  qabsor  10508  maxleast  10646  dvdslelemd  11122  odd2np1lem  11150  odd2np1  11151  isprm6  11404  uzdcinzz  11698  bj-findis  11874  nninfomnilem  11910
  Copyright terms: Public domain W3C validator