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

Theorem jaodan 792
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 712 . 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 703
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 704
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaodan  793  ordi  811  andi  813  dcor  930  ccase  959  mpjao3dan  1302  relop  4759  poltletr  5009  tfrlemisucaccv  6301  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  phplem3  6828  ssfilem  6849  diffitest  6861  reapmul1  8501  apsqgt0  8507  recexaplem2  8557  nnnn0addcl  9152  un0addcl  9155  un0mulcl  9156  elz2  9270  xrltso  9740  xaddnemnf  9801  xaddnepnf  9802  fzsplit2  9993  fzsuc2  10022  elfzp12  10042  expp1  10470  expnegap0  10471  expcllem  10474  mulexpzap  10503  expaddzap  10507  expmulzap  10509  bcpasc  10687  xrltmaxsup  11207  xrmaxaddlem  11210  summodc  11333  fsumsplit  11357  fprodsplitdc  11546  ef0lem  11610  odd2np1  11819  dvdslcm  12010  lcmeq0  12012  lcmcl  12013  lcmneg  12015  lcmgcd  12019  rpexp1i  12095  pcid  12264  lgsdir2lem4  13647  lgsdir2  13649  lgsdirnn0  13663  lgsdinn0  13664
  Copyright terms: Public domain W3C validator