Theorem syl23anc 1403

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  suppofss1d  8198  suppofss2d  8199  cnfcomlem  9666  ackbij1lem16  10224  div2subd  12047  symg2bas  19469  rhmpreimaprmidl  21490  psgndiflemA  21762  evl1expd  22516  evls1maplmhm  22548  oftpos  22620  restopn2  23345  tsmsxp  24323  blcld  24673  cnllycmp  25126  dvlipcn  26164  tanregt0  26715  ostthlem1  27802  nosupbnd1lem1  27883  nosupbnd2  27891  noinfbnd1lem1  27898  noinfbnd2  27906  ax5seglem6  29295  axcontlem4  29328  axcontlem7  29331  wwlksnextwrd  30257  drngidlhash  33750  qsdrngilem  33785  rsprprmprmidlb  33822  rprmirredb  33831  dfufd2lem  33848  lindsunlem  34023  lactlmhm  34033  pnfneige0  34350  qqhval2  34381  esumcocn  34479  carsgmon  34713  bnj1125  35389  heiborlem8  38497  2atjm  40247  1cvrat  40278  lvolnlelln  40386  lvolnlelpln  40387  4atlem3  40398  lplncvrlvol  40418  dalem39  40513  cdleme4a  41041  cdleme15  41080  cdleme16c  41082  cdleme19b  41106  cdleme19e  41109  cdleme20d  41114  cdleme20g  41117  cdleme20j  41120  cdleme20k  41121  cdleme20l2  41123  cdleme20l  41124  cdleme20m  41125  cdleme22e  41146  cdleme22eALTN  41147  cdleme22f  41148  cdleme27cl  41168  cdlemefr27cl  41205  mpaaeu  43905