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  8156  suppofss2d  8157  cnfcomlem  9620  ackbij1lem16  10156  div2subd  11979  symg2bas  19334  psgndiflemA  21568  evl1expd  22301  evls1maplmhm  22333  oftpos  22408  restopn2  23133  tsmsxp  24111  blcld  24461  cnllycmp  24923  dvlipcn  25967  tanregt0  26516  ostthlem1  27606  nosupbnd1lem1  27688  nosupbnd2  27696  noinfbnd1lem1  27703  noinfbnd2  27711  ax5seglem6  29019  axcontlem4  29052  axcontlem7  29055  wwlksnextwrd  29982  drngidlhash  33526  rhmpreimaprmidl  33543  qsdrngilem  33586  rsprprmprmidlb  33615  rprmirredb  33624  dfufd2lem  33641  lindsunlem  33801  lactlmhm  33811  pnfneige0  34128  qqhval2  34159  esumcocn  34257  carsgmon  34491  bnj1125  35167  heiborlem8  38063  2atjm  39815  1cvrat  39846  lvolnlelln  39954  lvolnlelpln  39955  4atlem3  39966  lplncvrlvol  39986  dalem39  40081  cdleme4a  40609  cdleme15  40648  cdleme16c  40650  cdleme19b  40674  cdleme19e  40677  cdleme20d  40682  cdleme20g  40685  cdleme20j  40688  cdleme20k  40689  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme22e  40714  cdleme22eALTN  40715  cdleme22f  40716  cdleme27cl  40736  cdlemefr27cl  40773  mpaaeu  43501