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  4573  smo11  6381  smoord  6382  omeulem1  6580  omopth2  6582  oaabs2  6643  elfiun  7183  r111  7447  r1pwss  7456  pwcfsdom  8205  winalim2  8318  xmullem  10584  xmulasslem  10605  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  ordtbas2  16921  ordtbas  16922  fmfnfmlem4  17652  dyadmbl  18955  scvxcvx  20280  perfectlem2  20469  ostth3  20787  poseq  24253  sltsolem1  24322  lineext  24699  fscgr  24703  colinbtwnle  24741  broutsideof2  24745  lineunray  24770  lineelsb2  24771  elicc3  26228  4atlem11  29798  dalawlem10  30069
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