Theorem jaodan 787

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

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaodan  788  ordi  806  andi  808  dcor  925  ccase  954  mpjao3dan  1297  relop  4753  poltletr  5003  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  phplem3  6816  ssfilem  6837  diffitest  6849  reapmul1  8489  apsqgt0  8495  recexaplem2  8545  nnnn0addcl  9140  un0addcl  9143  un0mulcl  9144  elz2  9258  xrltso  9728  xaddnemnf  9789  xaddnepnf  9790  fzsplit2  9981  fzsuc2  10010  elfzp12  10030  expp1  10458  expnegap0  10459  expcllem  10462  mulexpzap  10491  expaddzap  10495  expmulzap  10497  bcpasc  10675  xrltmaxsup  11194  xrmaxaddlem  11197  summodc  11320  fsumsplit  11344  fprodsplitdc  11533  ef0lem  11597  odd2np1  11806  dvdslcm  11997  lcmeq0  11999  lcmcl  12000  lcmneg  12002  lcmgcd  12006  rpexp1i  12082  pcid  12251  lgsdir2lem4  13532  lgsdir2  13534  lgsdirnn0  13548  lgsdinn0  13549