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

Theorem jaodan 710
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
jaodan.1  |-  ( (
ph  /\  ps )  ->  ch )
jaodan.2  |-  ( (
ph  /\  th )  ->  ch )
Assertion
Ref Expression
jaodan  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )

Proof of Theorem jaodan
StepHypRef Expression
1 jaodan.1 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
21ex 108 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 108 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
52, 4jaod 637 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
65imp 115 1  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    \/ 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:  mpjaodan  711  ordi  729  andi  731  dcor  843  ccase  871  mpjao3dan  1202  relop  4464  poltletr  4703  tfrlemisucaccv  5917  phplem3  6295  ssfiexmid  6314  diffitest  6321  reapmul1  7553  apsqgt0  7559  recexaplem2  7600  nnnn0addcl  8175  un0addcl  8178  un0mulcl  8179  elz2  8275  xrltso  8675  fzsplit2  8872  fzsuc2  8899  elfzp12  8919  expp1  9131  expnegap0  9132  expcllem  9135  mulexpzap  9164  expaddzap  9168  expmulzap  9170
  Copyright terms: Public domain W3C validator