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

Theorem ccased 1039
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 1038 . 2 (((𝜓𝜃) ∧ (𝜒𝜏)) → (𝜑𝜂))
109com12 32 1 (𝜑 → (((𝜓𝜃) ∧ (𝜒𝜏)) → 𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848
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 849
This theorem is referenced by:  fvf1pr  7327  resf1extb  7956  fpwwe2lem12  10682  mulge0  11781  zmulcl  12666  lcmabs  16642  pospo  18390  mulgass  19129  indistopon  23008  lgsdir2lem5  27373  outsideofeq  36131  weiunpo  36466  smprngopr  38059  cdlemg33  40713  monotoddzzfi  42954  acongtr  42990
  Copyright terms: Public domain W3C validator