Theorem syl23anc 1483

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

Hypotheses

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

Assertion

Ref	Expression
syl23anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl23anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 501	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1478	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  suppofss1d  7487  suppofss2d  7488  cnfcomlem  8763  ackbij1lem16  9262  div2subd  11056  symg2bas  18024  evl1expd  19923  psgndiflemA  20162  oftpos  20475  restopn2  21201  tsmsxp  22177  blcld  22529  metustexhalf  22580  cnllycmp  22974  dvlipcn  23976  tanregt0  24505  ostthlem1  25536  ax5seglem6  26034  axcontlem4  26067  axcontlem7  26070  wwlksnextwrd  27040  pnfneige0  30336  qqhval2  30365  esumcocn  30481  carsgmon  30715  bnj1125  31397  nosupbnd1lem1  32190  nosupbnd2  32198  heiborlem8  33948  2atjm  35253  1cvrat  35284  lvolnlelln  35392  lvolnlelpln  35393  4atlem3  35404  lplncvrlvol  35424  dalem39  35519  cdleme4a  36048  cdleme15  36087  cdleme16c  36089  cdleme19b  36113  cdleme19e  36116  cdleme20d  36121  cdleme20g  36124  cdleme20j  36127  cdleme20k  36128  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme22e  36153  cdleme22eALTN  36154  cdleme22f  36155  cdleme27cl  36175  cdlemefr27cl  36212  mpaaeu  38246