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

Theorem 3jaod 1246
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 1243 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 933
This theorem is referenced by:  3jaodan  1248  3jaao  1249  dfwe2  4589  smo11  6397  smoord  6398  omeulem1  6596  omopth2  6598  oaabs2  6659  elfiun  7199  r111  7463  r1pwss  7472  pwcfsdom  8221  winalim2  8334  xmullem  10600  xmulasslem  10621  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  ordtbas2  16937  ordtbas  16938  fmfnfmlem4  17668  dyadmbl  18971  scvxcvx  20296  perfectlem2  20485  ostth3  20803  poseq  24324  sltsolem1  24393  lineext  24771  fscgr  24775  colinbtwnle  24813  broutsideof2  24817  lineunray  24842  lineelsb2  24843  elicc3  26331  4atlem11  30420  dalawlem10  30691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936
  Copyright terms: Public domain W3C validator