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

Theorem 4casesdan 1028
Description: Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
Hypotheses
Ref Expression
4casesdan.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
4casesdan.2 ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃)
4casesdan.3 ((𝜑 ∧ (¬ 𝜓𝜒)) → 𝜃)
4casesdan.4 ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)
Assertion
Ref Expression
4casesdan (𝜑𝜃)

Proof of Theorem 4casesdan
StepHypRef Expression
1 4casesdan.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21expcom 450 . 2 ((𝜓𝜒) → (𝜑𝜃))
3 4casesdan.2 . . 3 ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃)
43expcom 450 . 2 ((𝜓 ∧ ¬ 𝜒) → (𝜑𝜃))
5 4casesdan.3 . . 3 ((𝜑 ∧ (¬ 𝜓𝜒)) → 𝜃)
65expcom 450 . 2 ((¬ 𝜓𝜒) → (𝜑𝜃))
7 4casesdan.4 . . 3 ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)
87expcom 450 . 2 ((¬ 𝜓 ∧ ¬ 𝜒) → (𝜑𝜃))
92, 4, 6, 84cases 1027 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
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-an 385
This theorem is referenced by:  unxpdomlem3  8331  mndifsplit  20644  cdleme41snaw  36266  dihord  37055  dihjat  37214
  Copyright terms: Public domain W3C validator