Theorem jaodan 809

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 729	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 124	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaodan  810  ordi  828  andi  830  dcor  948  ccase  977  mpjao3dan  1348  relop  4932  poltletr  5191  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  phplem3  7161  ssfilem  7183  ssfilemd  7185  diffitest  7197  pr1or2  7546  reapmul1  8931  apsqgt0  8937  recexaplem2  8988  nnnn0addcl  9604  un0addcl  9607  un0mulcl  9608  elz2  9725  xrltso  10214  xaddnemnf  10275  xaddnepnf  10276  fzsplit2  10471  fzsplit3  10474  fzsuc2  10502  elfzp12  10522  seqf1oglem2  10977  expp1  11003  expnegap0  11004  expcllem  11007  mulexpzap  11036  expaddzap  11040  expmulzap  11042  zzlesq  11166  bcpasc  11225  ccatass  11397  ccatrn  11398  ccatswrd  11463  ccatpfx  11494  cats1un  11514  xrltmaxsup  12047  xrmaxaddlem  12050  summodc  12174  fsumsplit  12198  fprodsplitdc  12387  ef0lem  12451  odd2np1  12664  dvdslcm  12871  lcmeq0  12873  lcmcl  12874  lcmneg  12876  lcmgcd  12880  rpexp1i  12957  pcid  13131  4sqlem16  13213  xpsfeq  13724  mulgneg  14001  mulgnn0z  14010  gsumunsnfd  14258  bposlem2  16329  lgsdir2lem4  16372  lgsdir2  16374  lgsdirnn0  16388  lgsdinn0  16389  idjudju  17269