Theorem syl23anc 1404

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  suppofss1d  8221  suppofss2d  8222  cnfcomlem  9700  ackbij1lem16  10312  div2subd  12143  symg2bas  19607  rhmpreimaprmidl  21635  psgndiflemA  21907  evl1expd  22663  evls1maplmhm  22695  oftpos  22767  restopn2  23495  tsmsxp  24474  blcld  24824  cnllycmp  25277  dvlipcn  26314  tanregt0  26867  ostthlem1  27954  nosupbnd1lem1  28065  nosupbnd2  28073  noinfbnd1lem1  28080  noinfbnd2  28088  angmgmaddov1  29388  ax5seglem6  29512  axcontlem4  29545  axcontlem7  29548  wwlksnextwrd  30486  drngidlhash  33983  qsdrngilem  34018  rsprprmprmidlb  34055  rprmirredb  34064  dfufd2lem  34081  lindsunlem  34256  lactlmhm  34266  pnfneige0  34583  qqhval2  34614  esumcocn  34712  carsgmon  34946  bnj1125  35622  heiborlem8  38753  2atjm  40503  1cvrat  40534  lvolnlelln  40642  lvolnlelpln  40643  4atlem3  40654  lplncvrlvol  40674  dalem39  40769  cdleme4a  41297  cdleme15  41336  cdleme16c  41338  cdleme19b  41362  cdleme19e  41365  cdleme20d  41370  cdleme20g  41373  cdleme20j  41376  cdleme20k  41377  cdleme20l2  41379  cdleme20l  41380  cdleme20m  41381  cdleme22e  41402  cdleme22eALTN  41403  cdleme22f  41404  cdleme27cl  41424  cdlemefr27cl  41461  mpaaeu  44152