Theorem syl23anc 1386

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  suppofss1d  8146  suppofss2d  8147  cnfcomlem  9615  ackbij1lem16  10151  div2subd  11976  symg2bas  19362  psgndiflemA  21579  evl1expd  22334  evls1maplmhm  22366  oftpos  22438  restopn2  23163  tsmsxp  24141  blcld  24491  cnllycmp  24944  dvlipcn  25982  tanregt0  26524  ostthlem1  27611  nosupbnd1lem1  27692  nosupbnd2  27700  noinfbnd1lem1  27707  noinfbnd2  27715  ax5seglem6  29023  axcontlem4  29056  axcontlem7  29059  wwlksnextwrd  29985  drngidlhash  33519  rhmpreimaprmidl  33536  qsdrngilem  33579  rsprprmprmidlb  33616  rprmirredb  33625  dfufd2lem  33642  lindsunlem  33818  lactlmhm  33828  pnfneige0  34145  qqhval2  34176  esumcocn  34274  carsgmon  34508  bnj1125  35187  heiborlem8  38198  2atjm  39950  1cvrat  39981  lvolnlelln  40089  lvolnlelpln  40090  4atlem3  40101  lplncvrlvol  40121  dalem39  40216  cdleme4a  40744  cdleme15  40783  cdleme16c  40785  cdleme19b  40809  cdleme19e  40812  cdleme20d  40817  cdleme20g  40820  cdleme20j  40823  cdleme20k  40824  cdleme20l2  40826  cdleme20l  40827  cdleme20m  40828  cdleme22e  40849  cdleme22eALTN  40850  cdleme22f  40851  cdleme27cl  40871  cdlemefr27cl  40908  mpaaeu  43608