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  8144  suppofss2d  8145  cnfcomlem  9614  ackbij1lem16  10147  div2subd  11968  symg2bas  19290  psgndiflemA  21526  evl1expd  22248  evls1maplmhm  22280  oftpos  22355  restopn2  23080  tsmsxp  24058  blcld  24409  cnllycmp  24871  dvlipcn  25915  tanregt0  26464  ostthlem1  27554  nosupbnd1lem1  27636  nosupbnd2  27644  noinfbnd1lem1  27651  noinfbnd2  27659  ax5seglem6  28897  axcontlem4  28930  axcontlem7  28933  wwlksnextwrd  29860  drngidlhash  33381  rhmpreimaprmidl  33398  qsdrngilem  33441  rsprprmprmidlb  33470  rprmirredb  33479  dfufd2lem  33496  lindsunlem  33596  lactlmhm  33606  pnfneige0  33917  qqhval2  33948  esumcocn  34046  carsgmon  34281  bnj1125  34958  heiborlem8  37797  2atjm  39424  1cvrat  39455  lvolnlelln  39563  lvolnlelpln  39564  4atlem3  39575  lplncvrlvol  39595  dalem39  39690  cdleme4a  40218  cdleme15  40257  cdleme16c  40259  cdleme19b  40283  cdleme19e  40286  cdleme20d  40291  cdleme20g  40294  cdleme20j  40297  cdleme20k  40298  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme22e  40323  cdleme22eALTN  40324  cdleme22f  40325  cdleme27cl  40345  cdlemefr27cl  40382  mpaaeu  43123