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  8020  suppofss2d  8021  cnfcomlem  9457  ackbij1lem16  9991  div2subd  11801  symg2bas  19000  psgndiflemA  20806  evl1expd  21511  oftpos  21601  restopn2  22328  tsmsxp  23306  blcld  23661  cnllycmp  24119  dvlipcn  25158  tanregt0  25695  ostthlem1  26775  ax5seglem6  27302  axcontlem4  27335  axcontlem7  27338  wwlksnextwrd  28262  rhmpreimaprmidl  31627  lindsunlem  31705  pnfneige0  31901  qqhval2  31932  esumcocn  32048  carsgmon  32281  bnj1125  32972  nosupbnd1lem1  33911  nosupbnd2  33919  noinfbnd1lem1  33926  noinfbnd2  33934  heiborlem8  35976  2atjm  37459  1cvrat  37490  lvolnlelln  37598  lvolnlelpln  37599  4atlem3  37610  lplncvrlvol  37630  dalem39  37725  cdleme4a  38253  cdleme15  38292  cdleme16c  38294  cdleme19b  38318  cdleme19e  38321  cdleme20d  38326  cdleme20g  38329  cdleme20j  38332  cdleme20k  38333  cdleme20l2  38335  cdleme20l  38336  cdleme20m  38337  cdleme22e  38358  cdleme22eALTN  38359  cdleme22f  38360  cdleme27cl  38380  cdlemefr27cl  38417  mpaaeu  40975