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  7603  addlocprlem  7903  nqprloc  7913  ltexprlemrl  7978  aptiprleml  8007  aptiprlemu  8008  elnn0z  9662  zaddcl  9689  zletric  9693  zlelttric  9694  zltnle  9695  zdceq  9725  zdcle  9726  zdclt  9727  nn01to3  10027  xposdif  10295  fzdcel  10455  qletric  10687  qlelttric  10688  qltnle  10689  qdceq  10690  qdclt  10691  frec2uzlt2d  10856  perfectlem2  16261  triap  17244  tridceq  17273