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

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 |- ( ( ph /\ ps ) -> ch )
2	1	ex 108	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 108	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 637	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 115	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

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  4486  poltletr  4725  tfrlemisucaccv  5939  phplem3  6317  ssfiexmid  6336  diffitest  6344  reapmul1  7586  apsqgt0  7592  recexaplem2  7633  nnnn0addcl  8212  un0addcl  8215  un0mulcl  8216  elz2  8312  xrltso  8717  fzsplit2  8914  fzsuc2  8941  elfzp12  8961  expp1  9262  expnegap0  9263  expcllem  9266  mulexpzap  9295  expaddzap  9299  expmulzap  9301