Theorem 3jaod 1338

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

Syntax hints:   -> wi 4   \/ w3o 1001

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 714

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004

This theorem is referenced by:  3jaodan  1340  3jaao  1342  issod  4410  nnawordex  6675  exmidontri2or  7428  addlocprlem  7722  nqprloc  7732  ltexprlemrl  7797  aptiprleml  7826  aptiprlemu  7827  elnn0z  9459  zaddcl  9486  zletric  9490  zlelttric  9491  zltnle  9492  zdceq  9522  zdcle  9523  zdclt  9524  nn01to3  9812  xposdif  10078  fzdcel  10236  qletric  10461  qlelttric  10462  qltnle  10463  qdceq  10464  qdclt  10465  frec2uzlt2d  10626  perfectlem2  15674  triap  16397  tridceq  16424