Theorem 3jaod 1299

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

Syntax hints:   -> wi 4   \/ w3o 972

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

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975

This theorem is referenced by:  3jaodan  1301  3jaao  1303  issod  4304  nnawordex  6508  exmidontri2or  7220  addlocprlem  7497  nqprloc  7507  ltexprlemrl  7572  aptiprleml  7601  aptiprlemu  7602  elnn0z  9225  zaddcl  9252  zletric  9256  zlelttric  9257  zltnle  9258  zdceq  9287  zdcle  9288  zdclt  9289  nn01to3  9576  xposdif  9839  fzdcel  9996  qletric  10200  qlelttric  10201  qltnle  10202  qdceq  10203  frec2uzlt2d  10360  triap  14061  tridceq  14088