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  7504  addlocprlem  7798  nqprloc  7808  ltexprlemrl  7873  aptiprleml  7902  aptiprlemu  7903  elnn0z  9537  zaddcl  9564  zletric  9568  zlelttric  9569  zltnle  9570  zdceq  9600  zdcle  9601  zdclt  9602  nn01to3  9896  xposdif  10162  fzdcel  10320  qletric  10547  qlelttric  10548  qltnle  10549  qdceq  10550  qdclt  10551  frec2uzlt2d  10712  perfectlem2  15797  triap  16744  tridceq  16772