MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jaod Structured version   Unicode version

Theorem 3jaod 1292
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
StepHypRef Expression
1 3jaod.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 3jaod.2 . 2  |-  ( ph  ->  ( th  ->  ch ) )
3 3jaod.3 . 2  |-  ( ph  ->  ( ta  ->  ch ) )
4 3jao 1289 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1228 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975
This theorem is referenced by:  3jaodan  1294  3jaao  1296  dfwe2  6612  smo11  7047  smoord  7048  omeulem1  7243  omopth2  7245  oaabs2  7306  elfiun  7902  r111  8205  r1pwss  8214  pwcfsdom  8970  winalim2  9086  xmullem  11468  xmulasslem  11489  xlemul1a  11492  xrsupsslem  11510  xrinfmsslem  11511  xrub  11515  ordtbas2  19560  ordtbas  19561  fmfnfmlem4  20326  dyadmbl  21877  scvxcvx  23181  perfectlem2  23371  ostth3  23689  poseq  29260  sltsolem1  29355  lineext  29653  fscgr  29657  colinbtwnle  29695  broutsideof2  29699  lineunray  29724  lineelsb2  29725  elicc3  30062  4atlem11  34806  dalawlem10  35077
  Copyright terms: Public domain W3C validator