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  4334  nnawordex  6548  exmidontri2or  7260  addlocprlem  7552  nqprloc  7562  ltexprlemrl  7627  aptiprleml  7656  aptiprlemu  7657  elnn0z  9284  zaddcl  9311  zletric  9315  zlelttric  9316  zltnle  9317  zdceq  9346  zdcle  9347  zdclt  9348  nn01to3  9635  xposdif  9900  fzdcel  10058  qletric  10262  qlelttric  10263  qltnle  10264  qdceq  10265  frec2uzlt2d  10422  triap  15162  tridceq  15189