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

Theorem 3jaod 1292
Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
3jaod.1
3jaod.2
3jaod.3
Assertion
Ref Expression
3jaod

Proof of Theorem 3jaod
StepHypRef Expression
1 3jaod.1 . 2
2 3jaod.2 . 2
3 3jaod.3 . 2
4 3jao 1289 . 2
51, 2, 3, 4syl3anc 1228 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/w3o 972
This theorem is referenced by:  3jaodan  1294  3jaao  1296  dfwe2  6617  smo11  7054  smoord  7055  omeulem1  7250  omopth2  7252  oaabs2  7313  elfiun  7910  r111  8214  r1pwss  8223  pwcfsdom  8979  winalim2  9095  xmullem  11485  xmulasslem  11506  xlemul1a  11509  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  ordtbas2  19692  ordtbas  19693  fmfnfmlem4  20458  dyadmbl  22009  scvxcvx  23315  perfectlem2  23505  ostth3  23823  poseq  29333  sltsolem1  29428  lineext  29726  fscgr  29730  colinbtwnle  29768  broutsideof2  29772  lineunray  29797  lineelsb2  29798  elicc3  30135  4atlem11  35333  dalawlem10  35604
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 974  df-3an 975
  Copyright terms: Public domain W3C validator