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

Theorem 3jaodan 1432
Description: Disjunction of three 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 416 . . 3 (𝜑 → (𝜓𝜒))
3 3jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 416 . . 3 (𝜑 → (𝜃𝜒))
5 3jaodan.3 . . . 4 ((𝜑𝜏) → 𝜒)
65ex 416 . . 3 (𝜑 → (𝜏𝜒))
72, 4, 63jaod 1430 . 2 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
87imp 410 1 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3o 1088
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 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091
This theorem is referenced by:  mpjao3dan  1433  onzsl  7643  zeo  12287  xrltnsym  12751  xrlttri  12753  xrlttr  12754  qbtwnxr  12814  xltnegi  12830  xaddcom  12854  xnegdi  12862  xsubge0  12875  xrub  12926  bpoly3  15644  blssioo  23716  ismbf2d  24561  itg2seq  24664  eliccioo  30949  3ccased  33401  lineelsb2  34213  sticksstones1  39853  dfxlim2v  43091
  Copyright terms: Public domain W3C validator