Theorem syl23anc 1379

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  suppofss1d  8183  suppofss2d  8184  cnfcomlem  9652  ackbij1lem16  10187  div2subd  12008  symg2bas  19323  psgndiflemA  21510  evl1expd  22232  evls1maplmhm  22264  oftpos  22339  restopn2  23064  tsmsxp  24042  blcld  24393  cnllycmp  24855  dvlipcn  25899  tanregt0  26448  ostthlem1  27538  nosupbnd1lem1  27620  nosupbnd2  27628  noinfbnd1lem1  27635  noinfbnd2  27643  ax5seglem6  28861  axcontlem4  28894  axcontlem7  28897  wwlksnextwrd  29827  drngidlhash  33405  rhmpreimaprmidl  33422  qsdrngilem  33465  rsprprmprmidlb  33494  rprmirredb  33503  dfufd2lem  33520  lindsunlem  33620  lactlmhm  33630  pnfneige0  33941  qqhval2  33972  esumcocn  34070  carsgmon  34305  bnj1125  34982  heiborlem8  37812  2atjm  39439  1cvrat  39470  lvolnlelln  39578  lvolnlelpln  39579  4atlem3  39590  lplncvrlvol  39610  dalem39  39705  cdleme4a  40233  cdleme15  40272  cdleme16c  40274  cdleme19b  40298  cdleme19e  40301  cdleme20d  40306  cdleme20g  40309  cdleme20j  40312  cdleme20k  40313  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme27cl  40360  cdlemefr27cl  40397  mpaaeu  43139