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  4464  nnawordex  6802  exmidontri2or  7602  addlocprlem  7902  nqprloc  7912  ltexprlemrl  7977  aptiprleml  8006  aptiprlemu  8007  elnn0z  9661  zaddcl  9688  zletric  9692  zlelttric  9693  zltnle  9694  zdceq  9724  zdcle  9725  zdclt  9726  nn01to3  10026  xposdif  10294  fzdcel  10454  qletric  10686  qlelttric  10687  qltnle  10688  qdceq  10689  qdclt  10690  frec2uzlt2d  10854  perfectlem2  16198  triap  17176  tridceq  17204