Theorem syl23anc 1377

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 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1372	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  suppofss1d  8191  suppofss2d  8192  cnfcomlem  9696  ackbij1lem16  10232  div2subd  12042  symg2bas  19262  psgndiflemA  21160  evl1expd  21871  oftpos  21961  restopn2  22688  tsmsxp  23666  blcld  24021  cnllycmp  24479  dvlipcn  25518  tanregt0  26055  ostthlem1  27137  nosupbnd1lem1  27218  nosupbnd2  27226  noinfbnd1lem1  27233  noinfbnd2  27241  ax5seglem6  28230  axcontlem4  28263  axcontlem7  28266  wwlksnextwrd  29189  drngidlhash  32597  rhmpreimaprmidl  32615  qsdrngilem  32653  lindsunlem  32768  evls1maplmhm  32820  pnfneige0  33000  qqhval2  33031  esumcocn  33147  carsgmon  33382  bnj1125  34072  heiborlem8  36772  2atjm  38402  1cvrat  38433  lvolnlelln  38541  lvolnlelpln  38542  4atlem3  38553  lplncvrlvol  38573  dalem39  38668  cdleme4a  39196  cdleme15  39235  cdleme16c  39237  cdleme19b  39261  cdleme19e  39264  cdleme20d  39269  cdleme20g  39272  cdleme20j  39275  cdleme20k  39276  cdleme20l2  39278  cdleme20l  39279  cdleme20m  39280  cdleme22e  39301  cdleme22eALTN  39302  cdleme22f  39303  cdleme27cl  39323  cdlemefr27cl  39360  mpaaeu  41974