Theorem 3jaod 1345

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

This proof depends on syntax axioms:   -> wi 4   \/ w3o 1008

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011

This theorem is used by:  3jaodan  1347  3jaao  1349  issod  4466  nnawordex  6807  exmidontri2or  7608  addlocprlem  7908  nqprloc  7918  ltexprlemrl  7983  aptiprleml  8012  aptiprlemu  8013  elnn0z  9666  zaddcl  9693  zletric  9697  zlelttric  9698  zltnle  9699  zdceq  9729  zdcle  9730  zdclt  9731  nn01to3  10032  xposdif  10300  fzdcel  10460  qletric  10692  qlelttric  10693  qltnle  10694  qdceq  10695  qdclt  10696  frec2uzlt2d  10861  perfectlem2  16317  triap  17301  tridceq  17330