Theorem syl23anc 1398

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  suppofss1d  8186  suppofss2d  8187  cnfcomlem  9656  ackbij1lem16  10192  div2subd  12019  symg2bas  19435  psgndiflemA  21655  evl1expd  22410  evls1maplmhm  22442  oftpos  22514  restopn2  23239  tsmsxp  24217  blcld  24567  cnllycmp  25020  dvlipcn  26058  tanregt0  26606  ostthlem1  27693  nosupbnd1lem1  27774  nosupbnd2  27782  noinfbnd1lem1  27789  noinfbnd2  27797  ax5seglem6  29137  axcontlem4  29170  axcontlem7  29173  wwlksnextwrd  30099  drngidlhash  33622  rhmpreimaprmidl  33640  qsdrngilem  33684  rsprprmprmidlb  33721  rprmirredb  33730  dfufd2lem  33747  lindsunlem  33923  lactlmhm  33933  pnfneige0  34250  qqhval2  34281  esumcocn  34379  carsgmon  34613  bnj1125  35289  heiborlem8  38322  2atjm  40074  1cvrat  40105  lvolnlelln  40213  lvolnlelpln  40214  4atlem3  40225  lplncvrlvol  40245  dalem39  40340  cdleme4a  40868  cdleme15  40907  cdleme16c  40909  cdleme19b  40933  cdleme19e  40936  cdleme20d  40941  cdleme20g  40944  cdleme20j  40947  cdleme20k  40948  cdleme20l2  40950  cdleme20l  40951  cdleme20m  40952  cdleme22e  40973  cdleme22eALTN  40974  cdleme22f  40975  cdleme27cl  40995  cdlemefr27cl  41032  mpaaeu  43732