Theorem syl23anc 1373

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  suppofss1d  7867  suppofss2d  7868  cnfcomlem  9161  ackbij1lem16  9656  div2subd  11465  symg2bas  18520  evl1expd  20507  psgndiflemA  20744  oftpos  21060  restopn2  21784  tsmsxp  22762  blcld  23114  cnllycmp  23559  dvlipcn  24590  tanregt0  25122  ostthlem1  26202  ax5seglem6  26719  axcontlem4  26752  axcontlem7  26755  wwlksnextwrd  27674  lindsunlem  31020  pnfneige0  31194  qqhval2  31223  esumcocn  31339  carsgmon  31572  bnj1125  32264  nosupbnd1lem1  33208  nosupbnd2  33216  heiborlem8  35095  2atjm  36580  1cvrat  36611  lvolnlelln  36719  lvolnlelpln  36720  4atlem3  36731  lplncvrlvol  36751  dalem39  36846  cdleme4a  37374  cdleme15  37413  cdleme16c  37415  cdleme19b  37439  cdleme19e  37442  cdleme20d  37447  cdleme20g  37450  cdleme20j  37453  cdleme20k  37454  cdleme20l2  37456  cdleme20l  37457  cdleme20m  37458  cdleme22e  37479  cdleme22eALTN  37480  cdleme22f  37481  cdleme27cl  37501  cdlemefr27cl  37538  mpaaeu  39748