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 ) )

This proof depends on syntax axioms:   -> wi 4   \/ w3o 1008

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

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

This theorem is used by:  3jaodan  1347  3jaao  1349  issod  4464  nnawordex  6802  exmidontri2or  7602  addlocprlem  7902  nqprloc  7912  ltexprlemrl  7977  aptiprleml  8006  aptiprlemu  8007  elnn0z  9657  zaddcl  9684  zletric  9688  zlelttric  9689  zltnle  9690  zdceq  9720  zdcle  9721  zdclt  9722  nn01to3  10017  xposdif  10284  fzdcel  10444  qletric  10676  qlelttric  10677  qltnle  10678  qdceq  10679  qdclt  10680  frec2uzlt2d  10841  perfectlem2  16114  triap  17078  tridceq  17106