Theorem 3jaod 1341

Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem 3jaod

Step	Hyp	Ref	Expression
1		3jaod.1	. 2 |- ( ph -> ( ps -> ch ) )
2		3jaod.2	. 2 |- ( ph -> ( th -> ch ) )
3		3jaod.3	. 2 |- ( ph -> ( ta -> ch ) )
4		3jao 1338	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ch ) /\ ( ta -> ch ) ) -> ( ( ps \/ th \/ ta ) -> ch ) )
5	1, 2, 3, 4	syl3anc 1274	1 |- ( ph -> ( ( ps \/ th \/ ta ) -> ch ) )

Syntax hints:   -> wi 4   \/ w3o 1004

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  df-3or 1006  df-3an 1007

This theorem is referenced by:  3jaodan  1343  3jaao  1345  issod  4422  nnawordex  6740  exmidontri2or  7521  addlocprlem  7815  nqprloc  7825  ltexprlemrl  7890  aptiprleml  7919  aptiprlemu  7920  elnn0z  9553  zaddcl  9580  zletric  9584  zlelttric  9585  zltnle  9586  zdceq  9616  zdcle  9617  zdclt  9618  nn01to3  9912  xposdif  10178  fzdcel  10337  qletric  10564  qlelttric  10565  qltnle  10566  qdceq  10567  qdclt  10568  frec2uzlt2d  10729  perfectlem2  15814  triap  16761  tridceq  16789