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  4830  prel12g  4869  injresinjlem  13823  prodmo  15969  nn0rppwr  16595  nn0expgcd  16598  nn0gcdsq  16786  symgextf1  19454  cnmsgnsubg  21613  zseo  28421  dvdsexpnn0  42348  zaddcom  42459  zmulcom  42463  kelac2lem  43053  omcl3g  43324  usgrexmpl2trifr  47932
  Copyright terms: Public domain W3C validator