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  8201  suppofss2d  8202  cnfcomlem  9711  ackbij1lem16  10246  div2subd  12065  symg2bas  19372  psgndiflemA  21559  evl1expd  22281  evls1maplmhm  22313  oftpos  22388  restopn2  23113  tsmsxp  24091  blcld  24442  cnllycmp  24904  dvlipcn  25949  tanregt0  26498  ostthlem1  27588  nosupbnd1lem1  27670  nosupbnd2  27678  noinfbnd1lem1  27685  noinfbnd2  27693  ax5seglem6  28859  axcontlem4  28892  axcontlem7  28895  wwlksnextwrd  29825  drngidlhash  33395  rhmpreimaprmidl  33412  qsdrngilem  33455  rsprprmprmidlb  33484  rprmirredb  33493  dfufd2lem  33510  lindsunlem  33610  lactlmhm  33620  pnfneige0  33928  qqhval2  33959  esumcocn  34057  carsgmon  34292  bnj1125  34969  heiborlem8  37788  2atjm  39410  1cvrat  39441  lvolnlelln  39549  lvolnlelpln  39550  4atlem3  39561  lplncvrlvol  39581  dalem39  39676  cdleme4a  40204  cdleme15  40243  cdleme16c  40245  cdleme19b  40269  cdleme19e  40272  cdleme20d  40277  cdleme20g  40280  cdleme20j  40283  cdleme20k  40284  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f  40311  cdleme27cl  40331  cdlemefr27cl  40368  mpaaeu  43121