Theorem syl23anc 1372

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl23anc.6	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl23anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl23anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 514	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1367	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  suppofss1d  7861  suppofss2d  7862  cnfcomlem  9155  ackbij1lem16  9650  div2subd  11459  symg2bas  18516  evl1expd  20503  psgndiflemA  20740  oftpos  21056  restopn2  21780  tsmsxp  22758  blcld  23110  cnllycmp  23555  dvlipcn  24588  tanregt0  25121  ostthlem1  26201  ax5seglem6  26718  axcontlem4  26751  axcontlem7  26754  wwlksnextwrd  27673  lindsunlem  31044  pnfneige0  31215  qqhval2  31244  esumcocn  31360  carsgmon  31593  bnj1125  32285  nosupbnd1lem1  33229  nosupbnd2  33237  heiborlem8  35129  2atjm  36614  1cvrat  36645  lvolnlelln  36753  lvolnlelpln  36754  4atlem3  36765  lplncvrlvol  36785  dalem39  36880  cdleme4a  37408  cdleme15  37447  cdleme16c  37449  cdleme19b  37473  cdleme19e  37476  cdleme20d  37481  cdleme20g  37484  cdleme20j  37487  cdleme20k  37488  cdleme20l2  37490  cdleme20l  37491  cdleme20m  37492  cdleme22e  37513  cdleme22eALTN  37514  cdleme22f  37515  cdleme27cl  37535  cdlemefr27cl  37572  mpaaeu  39826