Theorem syl23anc 1379

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 1374	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  suppofss1d  8134  suppofss2d  8135  cnfcomlem  9589  ackbij1lem16  10122  div2subd  11944  symg2bas  19303  psgndiflemA  21536  evl1expd  22258  evls1maplmhm  22290  oftpos  22365  restopn2  23090  tsmsxp  24068  blcld  24418  cnllycmp  24880  dvlipcn  25924  tanregt0  26473  ostthlem1  27563  nosupbnd1lem1  27645  nosupbnd2  27653  noinfbnd1lem1  27660  noinfbnd2  27668  ax5seglem6  28910  axcontlem4  28943  axcontlem7  28946  wwlksnextwrd  29873  drngidlhash  33394  rhmpreimaprmidl  33411  qsdrngilem  33454  rsprprmprmidlb  33483  rprmirredb  33492  dfufd2lem  33509  lindsunlem  33632  lactlmhm  33642  pnfneige0  33959  qqhval2  33990  esumcocn  34088  carsgmon  34322  bnj1125  34999  heiborlem8  37857  2atjm  39483  1cvrat  39514  lvolnlelln  39622  lvolnlelpln  39623  4atlem3  39634  lplncvrlvol  39654  dalem39  39749  cdleme4a  40277  cdleme15  40316  cdleme16c  40318  cdleme19b  40342  cdleme19e  40345  cdleme20d  40350  cdleme20g  40353  cdleme20j  40356  cdleme20k  40357  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme22e  40382  cdleme22eALTN  40383  cdleme22f  40384  cdleme27cl  40404  cdlemefr27cl  40441  mpaaeu  43182