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 511	. 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 395   ∧ 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 396  df-3an 1088

This theorem is referenced by:  suppofss1d  8193  suppofss2d  8194  cnfcomlem  9698  ackbij1lem16  10234  div2subd  12045  symg2bas  19302  psgndiflemA  21374  evl1expd  22085  oftpos  22175  restopn2  22902  tsmsxp  23880  blcld  24235  cnllycmp  24703  dvlipcn  25747  tanregt0  26285  ostthlem1  27367  nosupbnd1lem1  27448  nosupbnd2  27456  noinfbnd1lem1  27463  noinfbnd2  27471  ax5seglem6  28460  axcontlem4  28493  axcontlem7  28496  wwlksnextwrd  29419  drngidlhash  32827  rhmpreimaprmidl  32845  qsdrngilem  32883  lindsunlem  32998  evls1maplmhm  33050  pnfneige0  33230  qqhval2  33261  esumcocn  33377  carsgmon  33612  bnj1125  34302  heiborlem8  36990  2atjm  38620  1cvrat  38651  lvolnlelln  38759  lvolnlelpln  38760  4atlem3  38771  lplncvrlvol  38791  dalem39  38886  cdleme4a  39414  cdleme15  39453  cdleme16c  39455  cdleme19b  39479  cdleme19e  39482  cdleme20d  39487  cdleme20g  39490  cdleme20j  39493  cdleme20k  39494  cdleme20l2  39496  cdleme20l  39497  cdleme20m  39498  cdleme22e  39519  cdleme22eALTN  39520  cdleme22f  39521  cdleme27cl  39541  cdlemefr27cl  39578  mpaaeu  42195