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

Theorem 3jaod 1249
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 1246 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1185 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 936
This theorem is referenced by:  3jaodan  1251  3jaao  1252  dfwe2  4763  smo11  6627  smoord  6628  omeulem1  6826  omopth2  6828  oaabs2  6889  elfiun  7436  r111  7702  r1pwss  7711  pwcfsdom  8459  winalim2  8572  xmullem  10844  xmulasslem  10865  xlemul1a  10868  xrsupsslem  10886  xrinfmsslem  10887  xrub  10891  ordtbas2  17256  ordtbas  17257  fmfnfmlem4  17990  dyadmbl  19493  scvxcvx  20825  perfectlem2  21015  ostth3  21333  poseq  25529  sltsolem1  25624  lineext  26011  fscgr  26015  colinbtwnle  26053  broutsideof2  26057  lineunray  26082  lineelsb2  26083  elicc3  26321  4atlem11  30407  dalawlem10  30678
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 179  df-or 361  df-an 362  df-3or 938  df-3an 939
  Copyright terms: Public domain W3C validator