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  6806  exmidontri2or  7608  addlocprlem  7908  nqprloc  7918  ltexprlemrl  7983  aptiprleml  8012  aptiprlemu  8013  elnn0z  9668  zaddcl  9695  zletric  9699  zlelttric  9700  zltnle  9701  zdceq  9731  zdcle  9732  zdclt  9733  nn01to3  10033  xposdif  10301  fzdcel  10461  qletric  10693  qlelttric  10694  qltnle  10695  qdceq  10696  qdclt  10697  frec2uzlt2d  10862  perfectlem2  16300  triap  17284  tridceq  17313