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

Theorem jaodan 786
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 114 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 114 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
52, 4jaod 706 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
65imp 123 1  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaodan  787  ordi  805  andi  807  dcor  919  ccase  948  mpjao3dan  1285  relop  4684  poltletr  4934  tfrlemisucaccv  6215  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  phplem3  6741  ssfilem  6762  diffitest  6774  reapmul1  8350  apsqgt0  8356  recexaplem2  8406  nnnn0addcl  9000  un0addcl  9003  un0mulcl  9004  elz2  9115  xrltso  9575  xaddnemnf  9633  xaddnepnf  9634  fzsplit2  9823  fzsuc2  9852  elfzp12  9872  expp1  10293  expnegap0  10294  expcllem  10297  mulexpzap  10326  expaddzap  10330  expmulzap  10332  bcpasc  10505  xrltmaxsup  11019  xrmaxaddlem  11022  summodc  11145  fsumsplit  11169  ef0lem  11355  odd2np1  11559  dvdslcm  11739  lcmeq0  11741  lcmcl  11742  lcmneg  11744  lcmgcd  11748  rpexp1i  11821
  Copyright terms: Public domain W3C validator