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

Theorem jaodan 746
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 113 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 113 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
52, 4jaod 672 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
65imp 122 1  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    \/ 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:  mpjaodan  747  ordi  765  andi  767  dcor  881  ccase  910  mpjao3dan  1243  relop  4574  poltletr  4819  tfrlemisucaccv  6072  tfr1onlemsucaccv  6088  tfrcllemsucaccv  6101  phplem3  6550  ssfilem  6571  diffitest  6583  reapmul1  8048  apsqgt0  8054  recexaplem2  8095  nnnn0addcl  8673  un0addcl  8676  un0mulcl  8677  elz2  8788  xrltso  9235  fzsplit2  9433  fzsuc2  9460  elfzp12  9480  expp1  9927  expnegap0  9928  expcllem  9931  mulexpzap  9960  expaddzap  9964  expmulzap  9966  bcpasc  10139  isummo  10737  fsumsplit  10764  odd2np1  10966  dvdslcm  11144  lcmeq0  11146  lcmcl  11147  lcmneg  11149  lcmgcd  11153  rpexp1i  11226
  Copyright terms: Public domain W3C validator