Theorem 3jaod 1317

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

Syntax hints:   -> wi 4   \/ w3o 980

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

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983

This theorem is referenced by:  3jaodan  1319  3jaao  1321  issod  4367  nnawordex  6617  exmidontri2or  7357  addlocprlem  7650  nqprloc  7660  ltexprlemrl  7725  aptiprleml  7754  aptiprlemu  7755  elnn0z  9387  zaddcl  9414  zletric  9418  zlelttric  9419  zltnle  9420  zdceq  9450  zdcle  9451  zdclt  9452  nn01to3  9740  xposdif  10006  fzdcel  10164  qletric  10386  qlelttric  10387  qltnle  10388  qdceq  10389  qdclt  10390  frec2uzlt2d  10551  perfectlem2  15505  triap  16005  tridceq  16032