Theorem 3jaod 1294

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

Syntax hints:   -> wi 4   \/ w3o 967

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 699

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970

This theorem is referenced by:  3jaodan  1296  3jaao  1298  issod  4297  nnawordex  6496  exmidontri2or  7199  addlocprlem  7476  nqprloc  7486  ltexprlemrl  7551  aptiprleml  7580  aptiprlemu  7581  elnn0z  9204  zaddcl  9231  zletric  9235  zlelttric  9236  zltnle  9237  zdceq  9266  zdcle  9267  zdclt  9268  nn01to3  9555  xposdif  9818  fzdcel  9975  qletric  10179  qlelttric  10180  qltnle  10181  qdceq  10182  frec2uzlt2d  10339  triap  13918  tridceq  13945