Theorem syl23anc 1404

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  suppofss1d  8199  suppofss2d  8200  cnfcomlem  9678  ackbij1lem16  10283  div2subd  12112  symg2bas  19568  rhmpreimaprmidl  21596  psgndiflemA  21868  evl1expd  22624  evls1maplmhm  22656  oftpos  22728  restopn2  23456  tsmsxp  24435  blcld  24785  cnllycmp  25238  dvlipcn  26275  tanregt0  26830  ostthlem1  27917  nosupbnd1lem1  27998  nosupbnd2  28006  noinfbnd1lem1  28013  noinfbnd2  28021  angmgmaddov1  29321  ax5seglem6  29445  axcontlem4  29478  axcontlem7  29481  wwlksnextwrd  30419  drngidlhash  33916  qsdrngilem  33951  rsprprmprmidlb  33988  rprmirredb  33997  dfufd2lem  34014  lindsunlem  34189  lactlmhm  34199  pnfneige0  34516  qqhval2  34547  esumcocn  34645  carsgmon  34880  bnj1125  35556  heiborlem8  38672  2atjm  40422  1cvrat  40453  lvolnlelln  40561  lvolnlelpln  40562  4atlem3  40573  lplncvrlvol  40593  dalem39  40688  cdleme4a  41216  cdleme15  41255  cdleme16c  41257  cdleme19b  41281  cdleme19e  41284  cdleme20d  41289  cdleme20g  41292  cdleme20j  41295  cdleme20k  41296  cdleme20l2  41298  cdleme20l  41299  cdleme20m  41300  cdleme22e  41321  cdleme22eALTN  41322  cdleme22f  41323  cdleme27cl  41343  cdlemefr27cl  41380  mpaaeu  44095