Theorem 3jaod 1235

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

Syntax hints:   -> wi 4   \/ w3o 918

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921

This theorem is referenced by:  3jaodan  1237  3jaao  1239  issod  4074  nnawordex  6124  addlocprlem  6725  nqprloc  6735  ltexprlemrl  6800  aptiprleml  6829  aptiprlemu  6830  elnn0z  8364  zaddcl  8391  zletric  8395  zlelttric  8396  zltnle  8397  zdceq  8423  zdcle  8424  zdclt  8425  nn01to3  8702  fzdcel  9059  qletric  9253  qlelttric  9254  qltnle  9255  qdceq  9256  frec2uzlt2d  9406