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  8205  suppofss2d  8206  cnfcomlem  9681  ackbij1lem16  10239  div2subd  12068  symg2bas  19521  rhmpreimaprmidl  21543  psgndiflemA  21815  evl1expd  22571  evls1maplmhm  22603  oftpos  22675  restopn2  23403  tsmsxp  24382  blcld  24732  cnllycmp  25185  dvlipcn  26223  tanregt0  26774  ostthlem1  27861  nosupbnd1lem1  27942  nosupbnd2  27950  noinfbnd1lem1  27957  noinfbnd2  27965  angmndaddov1  29261  ax5seglem6  29377  axcontlem4  29410  axcontlem7  29413  wwlksnextwrd  30351  drngidlhash  33848  qsdrngilem  33883  rsprprmprmidlb  33920  rprmirredb  33929  dfufd2lem  33946  lindsunlem  34121  lactlmhm  34131  pnfneige0  34448  qqhval2  34479  esumcocn  34577  carsgmon  34812  bnj1125  35488  heiborlem8  38555  2atjm  40305  1cvrat  40336  lvolnlelln  40444  lvolnlelpln  40445  4atlem3  40456  lplncvrlvol  40476  dalem39  40571  cdleme4a  41099  cdleme15  41138  cdleme16c  41140  cdleme19b  41164  cdleme19e  41167  cdleme20d  41172  cdleme20g  41175  cdleme20j  41178  cdleme20k  41179  cdleme20l2  41181  cdleme20l  41182  cdleme20m  41183  cdleme22e  41204  cdleme22eALTN  41205  cdleme22f  41206  cdleme27cl  41226  cdlemefr27cl  41263  mpaaeu  43978