Theorem 3jaod 1304

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

Syntax hints:   -> wi 4   \/ w3o 977

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 709

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980

This theorem is referenced by:  3jaodan  1306  3jaao  1308  issod  4317  nnawordex  6525  exmidontri2or  7237  addlocprlem  7529  nqprloc  7539  ltexprlemrl  7604  aptiprleml  7633  aptiprlemu  7634  elnn0z  9260  zaddcl  9287  zletric  9291  zlelttric  9292  zltnle  9293  zdceq  9322  zdcle  9323  zdclt  9324  nn01to3  9611  xposdif  9876  fzdcel  10033  qletric  10237  qlelttric  10238  qltnle  10239  qdceq  10240  frec2uzlt2d  10397  triap  14548  tridceq  14575