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

Theorem 3jaodan 1434
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 449 . . 3 (𝜑 → (𝜓𝜒))
3 3jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 449 . . 3 (𝜑 → (𝜃𝜒))
5 3jaodan.3 . . . 4 ((𝜑𝜏) → 𝜒)
65ex 449 . . 3 (𝜑 → (𝜏𝜒))
72, 4, 63jaod 1432 . 2 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
87imp 444 1 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3o 1053
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 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056
This theorem is referenced by:  onzsl  7088  zeo  11501  xrltnsym  12008  xrlttri  12010  xrlttr  12011  qbtwnxr  12069  xltnegi  12085  xaddcom  12109  xnegdi  12116  xsubge0  12129  xrub  12180  bpoly3  14833  blssioo  22645  ismbf2d  23453  itg2seq  23554  eliccioo  29767  3ccased  31726  lineelsb2  32380  dfxlim2v  40391
  Copyright terms: Public domain W3C validator