Theorem 3jaod 1199

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 1196	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ch ) /\ ( ta -> ch ) ) -> ( ( ps \/ th \/ ta ) -> ch ) )
5	1, 2, 3, 4	syl3anc 1135	1 |- ( ph -> ( ( ps \/ th \/ ta ) -> ch ) )

Syntax hints:   -> wi 4   \/ w3o 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110  df-3or 886  df-3an 887

This theorem is referenced by:  3jaodan  1201  3jaao  1203  issod  4056  nnawordex  6101  addlocprlem  6633  nqprloc  6643  ltexprlemrl  6708  aptiprleml  6737  aptiprlemu  6738  elnn0z  8258  zaddcl  8285  zletric  8289  zlelttric  8290  zltnle  8291  zdceq  8316  zdcle  8317  zdclt  8318  nn01to3  8552  fzdcel  8904  qletric  9099  qlelttric  9100  qltnle  9101  qdceq  9102  frec2uzlt2d  9190