Theorem syl23anc 1402

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  suppofss1d  8199  suppofss2d  8200  cnfcomlem  9667  ackbij1lem16  10216  div2subd  12040  symg2bas  19462  rhmpreimaprmidl  21458  psgndiflemA  21730  evl1expd  22484  evls1maplmhm  22516  oftpos  22588  restopn2  23313  tsmsxp  24291  blcld  24641  cnllycmp  25094  dvlipcn  26132  tanregt0  26680  ostthlem1  27767  nosupbnd1lem1  27848  nosupbnd2  27856  noinfbnd1lem1  27863  noinfbnd2  27871  ax5seglem6  29250  axcontlem4  29283  axcontlem7  29286  wwlksnextwrd  30212  drngidlhash  33707  qsdrngilem  33742  rsprprmprmidlb  33779  rprmirredb  33788  dfufd2lem  33805  lindsunlem  33980  lactlmhm  33990  pnfneige0  34307  qqhval2  34338  esumcocn  34436  carsgmon  34670  bnj1125  35346  heiborlem8  38413  2atjm  40165  1cvrat  40196  lvolnlelln  40304  lvolnlelpln  40305  4atlem3  40316  lplncvrlvol  40336  dalem39  40431  cdleme4a  40959  cdleme15  40998  cdleme16c  41000  cdleme19b  41024  cdleme19e  41027  cdleme20d  41032  cdleme20g  41035  cdleme20j  41038  cdleme20k  41039  cdleme20l2  41041  cdleme20l  41042  cdleme20m  41043  cdleme22e  41064  cdleme22eALTN  41065  cdleme22f  41066  cdleme27cl  41086  cdlemefr27cl  41123  mpaaeu  43825