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

Theorem 3jaod 1282
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 1279 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1218 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 964
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 966  df-3an 967
This theorem is referenced by:  3jaodan  1284  3jaao  1286  dfwe2  6414  smo11  6846  smoord  6847  omeulem1  7042  omopth2  7044  oaabs2  7105  elfiun  7701  r111  8003  r1pwss  8012  pwcfsdom  8768  winalim2  8884  xmullem  11248  xmulasslem  11269  xlemul1a  11272  xrsupsslem  11290  xrinfmsslem  11291  xrub  11295  ordtbas2  18817  ordtbas  18818  fmfnfmlem4  19552  dyadmbl  21102  scvxcvx  22401  perfectlem2  22591  ostth3  22909  poseq  27736  sltsolem1  27831  lineext  28129  fscgr  28133  colinbtwnle  28171  broutsideof2  28175  lineunray  28200  lineelsb2  28201  elicc3  28538  4atlem11  33349  dalawlem10  33620
  Copyright terms: Public domain W3C validator