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  4440  nnawordex  6762  exmidontri2or  7553  addlocprlem  7850  nqprloc  7860  ltexprlemrl  7925  aptiprleml  7954  aptiprlemu  7955  elnn0z  9590  zaddcl  9617  zletric  9621  zlelttric  9622  zltnle  9623  zdceq  9653  zdcle  9654  zdclt  9655  nn01to3  9949  xposdif  10215  fzdcel  10374  qletric  10601  qlelttric  10602  qltnle  10603  qdceq  10604  qdclt  10605  frec2uzlt2d  10766  perfectlem2  15868  triap  16813  tridceq  16841