Theorem 3jaod 1345

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

Syntax hints:   -> wi 4   \/ w3o 1008

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 721

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011

This theorem is referenced by:  3jaodan  1347  3jaao  1349  issod  4459  nnawordex  6792  exmidontri2or  7592  addlocprlem  7892  nqprloc  7902  ltexprlemrl  7967  aptiprleml  7996  aptiprlemu  7997  elnn0z  9636  zaddcl  9663  zletric  9667  zlelttric  9668  zltnle  9669  zdceq  9699  zdcle  9700  zdclt  9701  nn01to3  9996  xposdif  10263  fzdcel  10423  qletric  10654  qlelttric  10655  qltnle  10656  qdceq  10657  qdclt  10658  frec2uzlt2d  10819  perfectlem2  16028  triap  16983  tridceq  17011