Theorem 3jaod 1315

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

Syntax hints:   -> wi 4   \/ w3o 979

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 710

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

This theorem is referenced by:  3jaodan  1317  3jaao  1319  issod  4350  nnawordex  6582  exmidontri2or  7303  addlocprlem  7595  nqprloc  7605  ltexprlemrl  7670  aptiprleml  7699  aptiprlemu  7700  elnn0z  9330  zaddcl  9357  zletric  9361  zlelttric  9362  zltnle  9363  zdceq  9392  zdcle  9393  zdclt  9394  nn01to3  9682  xposdif  9948  fzdcel  10106  qletric  10311  qlelttric  10312  qltnle  10313  qdceq  10314  qdclt  10315  frec2uzlt2d  10475  triap  15519  tridceq  15546