Theorem syl23anc 1376

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 1371	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  8227  suppofss2d  8228  cnfcomlem  9736  ackbij1lem16  10271  div2subd  12090  symg2bas  19424  psgndiflemA  21636  evl1expd  22364  evls1maplmhm  22396  oftpos  22473  restopn2  23200  tsmsxp  24178  blcld  24533  cnllycmp  25001  dvlipcn  26047  tanregt0  26595  ostthlem1  27685  nosupbnd1lem1  27767  nosupbnd2  27775  noinfbnd1lem1  27782  noinfbnd2  27790  ax5seglem6  28963  axcontlem4  28996  axcontlem7  28999  wwlksnextwrd  29926  drngidlhash  33441  rhmpreimaprmidl  33458  qsdrngilem  33501  rsprprmprmidlb  33530  rprmirredb  33539  dfufd2lem  33556  lindsunlem  33651  lactlmhm  33661  pnfneige0  33911  qqhval2  33944  esumcocn  34060  carsgmon  34295  bnj1125  34984  heiborlem8  37804  2atjm  39427  1cvrat  39458  lvolnlelln  39566  lvolnlelpln  39567  4atlem3  39578  lplncvrlvol  39598  dalem39  39693  cdleme4a  40221  cdleme15  40260  cdleme16c  40262  cdleme19b  40286  cdleme19e  40289  cdleme20d  40294  cdleme20g  40297  cdleme20j  40300  cdleme20k  40301  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme27cl  40348  cdlemefr27cl  40385  mpaaeu  43138