Theorem syl23anc 1484

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 555	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1479	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  suppofss1d  7502  suppofss2d  7503  cnfcomlem  8771  ackbij1lem16  9269  div2subd  11063  symg2bas  18038  evl1expd  19931  psgndiflemA  20169  oftpos  20480  restopn2  21203  tsmsxp  22179  blcld  22531  metustexhalf  22582  cnllycmp  22976  dvlipcn  23976  tanregt0  24505  ostthlem1  25536  ax5seglem6  26034  axcontlem4  26067  axcontlem7  26070  wwlksnextwrd  27036  pnfneige0  30327  qqhval2  30356  esumcocn  30472  carsgmon  30706  bnj1125  31388  nosupbnd1lem1  32181  nosupbnd2  32189  heiborlem8  33948  2atjm  35252  1cvrat  35283  lvolnlelln  35391  lvolnlelpln  35392  4atlem3  35403  lplncvrlvol  35423  dalem39  35518  cdleme4a  36047  cdleme15  36086  cdleme16c  36088  cdleme19b  36112  cdleme19e  36115  cdleme20d  36120  cdleme20g  36123  cdleme20j  36126  cdleme20k  36127  cdleme20l2  36129  cdleme20l  36130  cdleme20m  36131  cdleme22e  36152  cdleme22eALTN  36153  cdleme22f  36154  cdleme27cl  36174  cdlemefr27cl  36211  mpaaeu  38240