Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3ccased Structured version   Visualization version   GIF version

Theorem 3ccased 30661
Description: Triple disjunction form of ccased 984. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
Hypotheses
Ref Expression
3ccased.1 (𝜑 → ((𝜒𝜂) → 𝜓))
3ccased.2 (𝜑 → ((𝜒𝜁) → 𝜓))
3ccased.3 (𝜑 → ((𝜒𝜎) → 𝜓))
3ccased.4 (𝜑 → ((𝜃𝜂) → 𝜓))
3ccased.5 (𝜑 → ((𝜃𝜁) → 𝜓))
3ccased.6 (𝜑 → ((𝜃𝜎) → 𝜓))
3ccased.7 (𝜑 → ((𝜏𝜂) → 𝜓))
3ccased.8 (𝜑 → ((𝜏𝜁) → 𝜓))
3ccased.9 (𝜑 → ((𝜏𝜎) → 𝜓))
Assertion
Ref Expression
3ccased (𝜑 → (((𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜓))

Proof of Theorem 3ccased
StepHypRef Expression
1 3ccased.1 . . . . 5 (𝜑 → ((𝜒𝜂) → 𝜓))
21com12 32 . . . 4 ((𝜒𝜂) → (𝜑𝜓))
3 3ccased.2 . . . . 5 (𝜑 → ((𝜒𝜁) → 𝜓))
43com12 32 . . . 4 ((𝜒𝜁) → (𝜑𝜓))
5 3ccased.3 . . . . 5 (𝜑 → ((𝜒𝜎) → 𝜓))
65com12 32 . . . 4 ((𝜒𝜎) → (𝜑𝜓))
72, 4, 63jaodan 1385 . . 3 ((𝜒 ∧ (𝜂𝜁𝜎)) → (𝜑𝜓))
8 3ccased.4 . . . . 5 (𝜑 → ((𝜃𝜂) → 𝜓))
98com12 32 . . . 4 ((𝜃𝜂) → (𝜑𝜓))
10 3ccased.5 . . . . 5 (𝜑 → ((𝜃𝜁) → 𝜓))
1110com12 32 . . . 4 ((𝜃𝜁) → (𝜑𝜓))
12 3ccased.6 . . . . 5 (𝜑 → ((𝜃𝜎) → 𝜓))
1312com12 32 . . . 4 ((𝜃𝜎) → (𝜑𝜓))
149, 11, 133jaodan 1385 . . 3 ((𝜃 ∧ (𝜂𝜁𝜎)) → (𝜑𝜓))
15 3ccased.7 . . . . 5 (𝜑 → ((𝜏𝜂) → 𝜓))
1615com12 32 . . . 4 ((𝜏𝜂) → (𝜑𝜓))
17 3ccased.8 . . . . 5 (𝜑 → ((𝜏𝜁) → 𝜓))
1817com12 32 . . . 4 ((𝜏𝜁) → (𝜑𝜓))
19 3ccased.9 . . . . 5 (𝜑 → ((𝜏𝜎) → 𝜓))
2019com12 32 . . . 4 ((𝜏𝜎) → (𝜑𝜓))
2116, 18, 203jaodan 1385 . . 3 ((𝜏 ∧ (𝜂𝜁𝜎)) → (𝜑𝜓))
227, 14, 213jaoian 1384 . 2 (((𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → (𝜑𝜓))
2322com12 32 1 (𝜑 → (((𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3o 1029
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 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator