Theorem 3jaod 1304

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

Syntax hints:   -> wi 4   \/ w3o 977

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 709

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980

This theorem is referenced by:  3jaodan  1306  3jaao  1308  issod  4320  nnawordex  6530  exmidontri2or  7242  addlocprlem  7534  nqprloc  7544  ltexprlemrl  7609  aptiprleml  7638  aptiprlemu  7639  elnn0z  9266  zaddcl  9293  zletric  9297  zlelttric  9298  zltnle  9299  zdceq  9328  zdcle  9329  zdclt  9330  nn01to3  9617  xposdif  9882  fzdcel  10040  qletric  10244  qlelttric  10245  qltnle  10246  qdceq  10247  frec2uzlt2d  10404  triap  14780  tridceq  14807