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

Theorem 3ccased 31928
 Description: Triple disjunction form of ccased 1025. (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 1543 . . 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 1543 . . 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 1543 . . 3 ((𝜏 ∧ (𝜂𝜁𝜎)) → (𝜑𝜓))
227, 14, 213jaoian 1542 . 2 (((𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → (𝜑𝜓))
2322com12 32 1 (𝜑 → (((𝜒𝜃𝜏) ∧ (𝜂𝜁𝜎)) → 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∨ w3o 1071 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 1073  df-3an 1074 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator