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

Theorem 4casesdan 990
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 451 . 2 ((𝜓𝜒) → (𝜑𝜃))
3 4casesdan.2 . . 3 ((𝜑 ∧ (𝜓 ∧ ¬ 𝜒)) → 𝜃)
43expcom 451 . 2 ((𝜓 ∧ ¬ 𝜒) → (𝜑𝜃))
5 4casesdan.3 . . 3 ((𝜑 ∧ (¬ 𝜓𝜒)) → 𝜃)
65expcom 451 . 2 ((¬ 𝜓𝜒) → (𝜑𝜃))
7 4casesdan.4 . . 3 ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)
87expcom 451 . 2 ((¬ 𝜓 ∧ ¬ 𝜒) → (𝜑𝜃))
92, 4, 6, 84cases 989 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 386
This theorem is referenced by:  unxpdomlem3  8110  mndifsplit  20361  cdleme41snaw  35241  dihord  36030  dihjat  36189
  Copyright terms: Public domain W3C validator