Theorem jaod 369

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

Hypotheses

Ref	Expression
jaod.1	|- (ph -> (ps -> ch))
jaod.2	|- (ph -> (th -> ch))

Assertion

Ref	Expression
jaod	|- (ph -> ((ps \/ th) -> ch))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 |- (ph -> (ps -> ch))
2	1	com12 27	. . 3 |- (ps -> (ph -> ch))
3		jaod.2	. . . 4 |- (ph -> (th -> ch))
4	3	com12 27	. . 3 |- (th -> (ph -> ch))
5	2, 4	jaoi 368	. 2 |- ((ps \/ th) -> (ph -> ch))
6	5	com12 27	1 |- (ph -> ((ps \/ th) -> ch))

Syntax hints:   -> wi 4   \/ wo 357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359

This theorem is referenced by:  mpjaod  370  orel2  372  pm2.621  397  jaao  495  jaodan  760  pm2.63  763  ecase2d  906  ecase3d  909  dedlema  920  dedlemb  921  cad0  1400  psssstr  3376  opkth1g  4131  lenltfin  4470  ssfin  4471  evenodddisj  4517  vfinspss  4552  vinf  4556  fununi  5161  weds  5939  enprmaplem3  6079  leconnnc  6219  addceq0  6220  nclenn  6250  muc0or  6253  ncslesuc  6268  nnc3n3p1  6279  nchoicelem6  6295  dmfrec  6317  fnfreclem2  6319