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  4354  nnawordex  6587  exmidontri2or  7310  addlocprlem  7602  nqprloc  7612  ltexprlemrl  7677  aptiprleml  7706  aptiprlemu  7707  elnn0z  9339  zaddcl  9366  zletric  9370  zlelttric  9371  zltnle  9372  zdceq  9401  zdcle  9402  zdclt  9403  nn01to3  9691  xposdif  9957  fzdcel  10115  qletric  10331  qlelttric  10332  qltnle  10333  qdceq  10334  qdclt  10335  frec2uzlt2d  10496  perfectlem2  15236  triap  15673  tridceq  15700