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

Theorem ccase 1037
Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
Hypotheses
Ref Expression
ccase.1 ((𝜑𝜓) → 𝜏)
ccase.2 ((𝜒𝜓) → 𝜏)
ccase.3 ((𝜑𝜃) → 𝜏)
ccase.4 ((𝜒𝜃) → 𝜏)
Assertion
Ref Expression
ccase (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)

Proof of Theorem ccase
StepHypRef Expression
1 ccase.1 . . 3 ((𝜑𝜓) → 𝜏)
2 ccase.2 . . 3 ((𝜒𝜓) → 𝜏)
31, 2jaoian 958 . 2 (((𝜑𝜒) ∧ 𝜓) → 𝜏)
4 ccase.3 . . 3 ((𝜑𝜃) → 𝜏)
5 ccase.4 . . 3 ((𝜒𝜃) → 𝜏)
64, 5jaoian 958 . 2 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
73, 6jaodan 959 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:  ccased  1038  ccase2  1039  ssprsseq  4824  prel12g  4863  injresinjlem  13827  prodmo  15973  nn0rppwr  16599  nn0expgcd  16602  nn0gcdsq  16790  symgextf1  19440  cnmsgnsubg  21596  zseo  28407  dvdsexpnn0  42374  zaddcom  42487  zmulcom  42491  kelac2lem  43081  omcl3g  43352  usgrexmpl2trifr  48001
  Copyright terms: Public domain W3C validator