Theorem jaodan 805

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 115	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 115	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 725	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 124	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  806  ordi  824  andi  826  dcor  944  ccase  973  mpjao3dan  1344  relop  4886  poltletr  5144  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  phplem3  7083  ssfilem  7105  ssfilemd  7107  diffitest  7119  pr1or2  7459  reapmul1  8834  apsqgt0  8840  recexaplem2  8891  nnnn0addcl  9491  un0addcl  9494  un0mulcl  9495  elz2  9612  xrltso  10092  xaddnemnf  10153  xaddnepnf  10154  fzsplit2  10347  fzsuc2  10376  elfzp12  10396  seqf1oglem2  10845  expp1  10871  expnegap0  10872  expcllem  10875  mulexpzap  10904  expaddzap  10908  expmulzap  10910  zzlesq  11033  bcpasc  11091  ccatass  11251  ccatrn  11252  ccatswrd  11317  ccatpfx  11348  cats1un  11368  xrltmaxsup  11897  xrmaxaddlem  11900  summodc  12024  fsumsplit  12048  fprodsplitdc  12237  ef0lem  12301  odd2np1  12514  dvdslcm  12721  lcmeq0  12723  lcmcl  12724  lcmneg  12726  lcmgcd  12730  rpexp1i  12806  pcid  12977  4sqlem16  13059  xpsfeq  13508  mulgneg  13807  mulgnn0z  13816  lgsdir2lem4  15850  lgsdir2  15852  lgsdirnn0  15866  lgsdinn0  15867