Theorem 3jaod 1317

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

Syntax hints:   -> wi 4   \/ w3o 980

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 711

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983

This theorem is referenced by:  3jaodan  1319  3jaao  1321  issod  4384  nnawordex  6638  exmidontri2or  7389  addlocprlem  7683  nqprloc  7693  ltexprlemrl  7758  aptiprleml  7787  aptiprlemu  7788  elnn0z  9420  zaddcl  9447  zletric  9451  zlelttric  9452  zltnle  9453  zdceq  9483  zdcle  9484  zdclt  9485  nn01to3  9773  xposdif  10039  fzdcel  10197  qletric  10421  qlelttric  10422  qltnle  10423  qdceq  10424  qdclt  10425  frec2uzlt2d  10586  perfectlem2  15587  triap  16170  tridceq  16197