Theorem 3jaod 1315

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

Syntax hints:   -> wi 4   \/ w3o 979

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 710

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

This theorem is referenced by:  3jaodan  1317  3jaao  1319  issod  4351  nnawordex  6584  exmidontri2or  7305  addlocprlem  7597  nqprloc  7607  ltexprlemrl  7672  aptiprleml  7701  aptiprlemu  7702  elnn0z  9333  zaddcl  9360  zletric  9364  zlelttric  9365  zltnle  9366  zdceq  9395  zdcle  9396  zdclt  9397  nn01to3  9685  xposdif  9951  fzdcel  10109  qletric  10314  qlelttric  10315  qltnle  10316  qdceq  10317  qdclt  10318  frec2uzlt2d  10478  triap  15589  tridceq  15616