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

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

Proof of Theorem 3jaodan
StepHypRef Expression
1 3jaodan.1 . . . 4
21ex 434 . . 3
3 3jaodan.2 . . . 4
43ex 434 . . 3
5 3jaodan.3 . . . 4
65ex 434 . . 3
72, 4, 63jaod 1292 . 2
87imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  \/w3o 972
This theorem is referenced by:  onzsl  6681  zeo  10973  xrltnsym  11372  xrlttri  11374  xrlttr  11375  qbtwnxr  11428  xltnegi  11444  xaddcom  11466  xnegdi  11469  xsubge0  11482  xrub  11532  blssioo  21300  ismbf2d  22048  itg2seq  22149  eliccioo  27627  3ccased  29096  lineelsb2  29798  bpoly3  29820
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