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

Theorem ccased 1038
Description: Deduction for combining cases. (Contributed by NM, 9-May-2004.)
Hypotheses
Ref Expression
ccased.1 (𝜑 → ((𝜓𝜒) → 𝜂))
ccased.2 (𝜑 → ((𝜃𝜒) → 𝜂))
ccased.3 (𝜑 → ((𝜓𝜏) → 𝜂))
ccased.4 (𝜑 → ((𝜃𝜏) → 𝜂))
Assertion
Ref Expression
ccased (𝜑 → (((𝜓𝜃) ∧ (𝜒𝜏)) → 𝜂))

Proof of Theorem ccased
StepHypRef Expression
1 ccased.1 . . . 4 (𝜑 → ((𝜓𝜒) → 𝜂))
21com12 32 . . 3 ((𝜓𝜒) → (𝜑𝜂))
3 ccased.2 . . . 4 (𝜑 → ((𝜃𝜒) → 𝜂))
43com12 32 . . 3 ((𝜃𝜒) → (𝜑𝜂))
5 ccased.3 . . . 4 (𝜑 → ((𝜓𝜏) → 𝜂))
65com12 32 . . 3 ((𝜓𝜏) → (𝜑𝜂))
7 ccased.4 . . . 4 (𝜑 → ((𝜃𝜏) → 𝜂))
87com12 32 . . 3 ((𝜃𝜏) → (𝜑𝜂))
92, 4, 6, 8ccase 1037 . 2 (((𝜓𝜃) ∧ (𝜒𝜏)) → (𝜑𝜂))
109com12 32 1 (𝜑 → (((𝜓𝜃) ∧ (𝜒𝜏)) → 𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 847
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 207  df-an 396  df-or 848
This theorem is referenced by:  fvf1pr  7326  fpwwe2lem12  10679  mulge0  11778  zmulcl  12663  lcmabs  16638  pospo  18402  mulgass  19141  indistopon  23023  lgsdir2lem5  27387  outsideofeq  36111  weiunpo  36447  smprngopr  38038  cdlemg33  40693  monotoddzzfi  42930  acongtr  42966
  Copyright terms: Public domain W3C validator