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

Theorem 3jaodan 1545
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 398 . . 3 (𝜑 → (𝜓𝜒))
3 3jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 398 . . 3 (𝜑 → (𝜃𝜒))
5 3jaodan.3 . . . 4 ((𝜑𝜏) → 𝜒)
65ex 398 . . 3 (𝜑 → (𝜏𝜒))
72, 4, 63jaod 1543 . 2 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
87imp 394 1 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3o 1097
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 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100
This theorem is referenced by:  onzsl  7214  zeo  11687  xrltnsym  12192  xrlttri  12194  xrlttr  12195  qbtwnxr  12255  xltnegi  12271  xaddcom  12295  xnegdi  12302  xsubge0  12315  xrub  12366  bpoly3  15017  blssioo  22838  ismbf2d  23648  itg2seq  23750  eliccioo  29996  3ccased  31955  lineelsb2  32609  dfxlim2v  40597
  Copyright terms: Public domain W3C validator