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  8186  suppofss2d  8187  cnfcomlem  9659  ackbij1lem16  10194  div2subd  12015  symg2bas  19330  psgndiflemA  21517  evl1expd  22239  evls1maplmhm  22271  oftpos  22346  restopn2  23071  tsmsxp  24049  blcld  24400  cnllycmp  24862  dvlipcn  25906  tanregt0  26455  ostthlem1  27545  nosupbnd1lem1  27627  nosupbnd2  27635  noinfbnd1lem1  27642  noinfbnd2  27650  ax5seglem6  28868  axcontlem4  28901  axcontlem7  28904  wwlksnextwrd  29834  drngidlhash  33412  rhmpreimaprmidl  33429  qsdrngilem  33472  rsprprmprmidlb  33501  rprmirredb  33510  dfufd2lem  33527  lindsunlem  33627  lactlmhm  33637  pnfneige0  33948  qqhval2  33979  esumcocn  34077  carsgmon  34312  bnj1125  34989  heiborlem8  37819  2atjm  39446  1cvrat  39477  lvolnlelln  39585  lvolnlelpln  39586  4atlem3  39597  lplncvrlvol  39617  dalem39  39712  cdleme4a  40240  cdleme15  40279  cdleme16c  40281  cdleme19b  40305  cdleme19e  40308  cdleme20d  40313  cdleme20g  40316  cdleme20j  40319  cdleme20k  40320  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme27cl  40367  cdlemefr27cl  40404  mpaaeu  43146