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

Theorem jaodan 721
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 112 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 112 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
52, 4jaod 647 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
65imp 119 1  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    \/ 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:  mpjaodan  722  ordi  740  andi  742  dcor  854  ccase  882  mpjao3dan  1213  relop  4513  poltletr  4752  tfrlemisucaccv  5969  phplem3  6347  ssfiexmid  6366  diffitest  6374  reapmul1  7659  apsqgt0  7665  recexaplem2  7706  nnnn0addcl  8268  un0addcl  8271  un0mulcl  8272  elz2  8369  xrltso  8817  fzsplit2  9015  fzsuc2  9042  elfzp12  9062  expp1  9426  expnegap0  9427  expcllem  9430  mulexpzap  9459  expaddzap  9463  expmulzap  9465  bcpasc  9633  odd2np1  10183
  Copyright terms: Public domain W3C validator