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

Theorem 3jaodan 1430
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 412 . . 3 (𝜑 → (𝜓𝜒))
3 3jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 412 . . 3 (𝜑 → (𝜃𝜒))
5 3jaodan.3 . . . 4 ((𝜑𝜏) → 𝜒)
65ex 412 . . 3 (𝜑 → (𝜏𝜒))
72, 4, 63jaod 1428 . 2 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
87imp 406 1 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3o 1085
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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088
This theorem is referenced by:  mpjao3dan  1431  onzsl  7867  zeo  12702  xrltnsym  13176  xrlttri  13178  xrlttr  13179  qbtwnxr  13239  xltnegi  13255  xaddcom  13279  xnegdi  13287  xsubge0  13300  xrub  13351  bpoly3  16091  blssioo  24831  ismbf2d  25689  itg2seq  25792  eliccioo  32898  3ccased  35699  lineelsb2  36130  sticksstones1  42128  dfxlim2v  45803  usgrexmpl2trifr  47932
  Copyright terms: Public domain W3C validator