Theorem syl23anc 1405

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 1400	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  8246  suppofss2d  8247  cnfcomlem  9724  ackbij1lem16  10336  div2subd  12167  symg2bas  19634  rhmpreimaprmidl  21662  psgndiflemA  21934  evl1expd  22690  evls1maplmhm  22722  oftpos  22794  restopn2  23522  tsmsxp  24501  blcld  24851  cnllycmp  25304  dvlipcn  26341  tanregt0  26894  ostthlem1  27981  nosupbnd1lem1  28092  nosupbnd2  28100  noinfbnd1lem1  28107  noinfbnd2  28115  angmgmaddov1  29415  ax5seglem6  29539  axcontlem4  29572  axcontlem7  29575  wwlksnextwrd  30513  drngidlhash  34050  qsdrngilem  34085  rsprprmprmidlb  34122  rprmirredb  34131  dfufd2lem  34148  lindsunlem  34323  lactlmhm  34333  pnfneige0  34650  qqhval2  34681  esumcocn  34779  carsgmon  35013  bnj1125  35689  heiborlem8  38943  2atjm  40693  1cvrat  40724  lvolnlelln  40832  lvolnlelpln  40833  4atlem3  40844  lplncvrlvol  40864  dalem39  40959  cdleme4a  41487  cdleme15  41526  cdleme16c  41528  cdleme19b  41552  cdleme19e  41555  cdleme20d  41560  cdleme20g  41563  cdleme20j  41566  cdleme20k  41567  cdleme20l2  41569  cdleme20l  41570  cdleme20m  41571  cdleme22e  41592  cdleme22eALTN  41593  cdleme22f  41594  cdleme27cl  41614  cdlemefr27cl  41651  mpaaeu  44342