Theorem syl23anc 1374

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 515	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1369	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  suppofss1d  7851  suppofss2d  7852  cnfcomlem  9146  ackbij1lem16  9646  div2subd  11455  symg2bas  18513  psgndiflemA  20290  evl1expd  20969  oftpos  21057  restopn2  21782  tsmsxp  22760  blcld  23112  cnllycmp  23561  dvlipcn  24597  tanregt0  25131  ostthlem1  26211  ax5seglem6  26728  axcontlem4  26761  axcontlem7  26764  wwlksnextwrd  27683  rhmpreimaprmidl  31035  lindsunlem  31108  pnfneige0  31304  qqhval2  31333  esumcocn  31449  carsgmon  31682  bnj1125  32374  nosupbnd1lem1  33321  nosupbnd2  33329  heiborlem8  35256  2atjm  36741  1cvrat  36772  lvolnlelln  36880  lvolnlelpln  36881  4atlem3  36892  lplncvrlvol  36912  dalem39  37007  cdleme4a  37535  cdleme15  37574  cdleme16c  37576  cdleme19b  37600  cdleme19e  37603  cdleme20d  37608  cdleme20g  37611  cdleme20j  37614  cdleme20k  37615  cdleme20l2  37617  cdleme20l  37618  cdleme20m  37619  cdleme22e  37640  cdleme22eALTN  37641  cdleme22f  37642  cdleme27cl  37662  cdlemefr27cl  37699  mpaaeu  40094