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

Theorem 3jaodan 1392
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 450 . . 3 (𝜑 → (𝜓𝜒))
3 3jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 450 . . 3 (𝜑 → (𝜃𝜒))
5 3jaodan.3 . . . 4 ((𝜑𝜏) → 𝜒)
65ex 450 . . 3 (𝜑 → (𝜏𝜒))
72, 4, 63jaod 1390 . 2 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
87imp 445 1 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3o 1035
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 385  df-an 386  df-3or 1037  df-3an 1038
This theorem is referenced by:  onzsl  7031  zeo  11448  xrltnsym  11955  xrlttri  11957  xrlttr  11958  qbtwnxr  12016  xltnegi  12032  xaddcom  12056  xnegdi  12063  xsubge0  12076  xrub  12127  bpoly3  14770  blssioo  22579  ismbf2d  23389  itg2seq  23490  eliccioo  29613  3ccased  31575  lineelsb2  32230
  Copyright terms: Public domain W3C validator