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

Theorem 3jaod 1296
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 1293 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1232 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 975
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 187  df-or 370  df-an 371  df-3or 977  df-3an 978
This theorem is referenced by:  3jaodan  1298  3jaao  1300  dfwe2  6601  smo11  7070  smoord  7071  omeulem1  7270  omopth2  7272  oaabs2  7333  elfiun  7926  r111  8227  r1pwss  8236  pwcfsdom  8992  winalim2  9106  xmullem  11511  xmulasslem  11532  xlemul1a  11535  xrsupsslem  11553  xrinfmsslem  11554  xrub  11558  ordtbas2  19987  ordtbas  19988  fmfnfmlem4  20752  dyadmbl  22303  scvxcvx  23643  perfectlem2  23888  ostth3  24206  poseq  30077  sltsolem1  30141  lineext  30427  fscgr  30431  colinbtwnle  30469  broutsideof2  30473  lineunray  30498  lineelsb2  30499  elicc3  30558  4atlem11  32639  dalawlem10  32910  frege129d  35755  perfectALTVlem2  37810
  Copyright terms: Public domain W3C validator