Theorem syl23anc 1380

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 1375	1 ⊢ (𝜑 → 𝜁)

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

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 1089

This theorem is referenced by:  suppofss1d  8147  suppofss2d  8148  cnfcomlem  9611  ackbij1lem16  10147  div2subd  11972  symg2bas  19359  psgndiflemA  21591  evl1expd  22320  evls1maplmhm  22352  oftpos  22427  restopn2  23152  tsmsxp  24130  blcld  24480  cnllycmp  24933  dvlipcn  25971  tanregt0  26516  ostthlem1  27604  nosupbnd1lem1  27686  nosupbnd2  27694  noinfbnd1lem1  27701  noinfbnd2  27709  ax5seglem6  29017  axcontlem4  29050  axcontlem7  29053  wwlksnextwrd  29980  drngidlhash  33509  rhmpreimaprmidl  33526  qsdrngilem  33569  rsprprmprmidlb  33598  rprmirredb  33607  dfufd2lem  33624  lindsunlem  33784  lactlmhm  33794  pnfneige0  34111  qqhval2  34142  esumcocn  34240  carsgmon  34474  bnj1125  35150  heiborlem8  38153  2atjm  39905  1cvrat  39936  lvolnlelln  40044  lvolnlelpln  40045  4atlem3  40056  lplncvrlvol  40076  dalem39  40171  cdleme4a  40699  cdleme15  40738  cdleme16c  40740  cdleme19b  40764  cdleme19e  40767  cdleme20d  40772  cdleme20g  40775  cdleme20j  40778  cdleme20k  40779  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme27cl  40826  cdlemefr27cl  40863  mpaaeu  43596