Theorem syl23anc 1376

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  suppofss1d  8091  suppofss2d  8092  cnfcomlem  9557  ackbij1lem16  10093  div2subd  11903  symg2bas  19097  psgndiflemA  20913  evl1expd  21618  oftpos  21708  restopn2  22435  tsmsxp  23413  blcld  23768  cnllycmp  24226  dvlipcn  25265  tanregt0  25802  ostthlem1  26882  nosupbnd1lem1  26963  nosupbnd2  26971  noinfbnd1lem1  26978  noinfbnd2  26986  ax5seglem6  27592  axcontlem4  27625  axcontlem7  27628  wwlksnextwrd  28551  rhmpreimaprmidl  31924  lindsunlem  32003  pnfneige0  32199  qqhval2  32230  esumcocn  32346  carsgmon  32581  bnj1125  33271  heiborlem8  36132  2atjm  37764  1cvrat  37795  lvolnlelln  37903  lvolnlelpln  37904  4atlem3  37915  lplncvrlvol  37935  dalem39  38030  cdleme4a  38558  cdleme15  38597  cdleme16c  38599  cdleme19b  38623  cdleme19e  38626  cdleme20d  38631  cdleme20g  38634  cdleme20j  38637  cdleme20k  38638  cdleme20l2  38640  cdleme20l  38641  cdleme20m  38642  cdleme22e  38663  cdleme22eALTN  38664  cdleme22f  38665  cdleme27cl  38685  cdlemefr27cl  38722  mpaaeu  41289