Theorem 3jaod 1282

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

Syntax hints:   -> wi 4   \/ w3o 961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964

This theorem is referenced by:  3jaodan  1284  3jaao  1286  issod  4236  nnawordex  6417  addlocprlem  7336  nqprloc  7346  ltexprlemrl  7411  aptiprleml  7440  aptiprlemu  7441  elnn0z  9060  zaddcl  9087  zletric  9091  zlelttric  9092  zltnle  9093  zdceq  9119  zdcle  9120  zdclt  9121  nn01to3  9402  xposdif  9658  fzdcel  9813  qletric  10014  qlelttric  10015  qltnle  10016  qdceq  10017  frec2uzlt2d  10170  triap  13213