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  10125  div2subd  11947  symg2bas  19305  psgndiflemA  21538  evl1expd  22260  evls1maplmhm  22292  oftpos  22367  restopn2  23092  tsmsxp  24070  blcld  24420  cnllycmp  24882  dvlipcn  25926  tanregt0  26475  ostthlem1  27565  nosupbnd1lem1  27647  nosupbnd2  27655  noinfbnd1lem1  27662  noinfbnd2  27670  ax5seglem6  28912  axcontlem4  28945  axcontlem7  28948  wwlksnextwrd  29875  drngidlhash  33399  rhmpreimaprmidl  33416  qsdrngilem  33459  rsprprmprmidlb  33488  rprmirredb  33497  dfufd2lem  33514  lindsunlem  33637  lactlmhm  33647  pnfneige0  33964  qqhval2  33995  esumcocn  34093  carsgmon  34327  bnj1125  35004  heiborlem8  37857  2atjm  39543  1cvrat  39574  lvolnlelln  39682  lvolnlelpln  39683  4atlem3  39694  lplncvrlvol  39714  dalem39  39809  cdleme4a  40337  cdleme15  40376  cdleme16c  40378  cdleme19b  40402  cdleme19e  40405  cdleme20d  40410  cdleme20g  40413  cdleme20j  40416  cdleme20k  40417  cdleme20l2  40419  cdleme20l  40420  cdleme20m  40421  cdleme22e  40442  cdleme22eALTN  40443  cdleme22f  40444  cdleme27cl  40464  cdlemefr27cl  40501  mpaaeu  43242