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 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 1372	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  8245  suppofss2d  8246  cnfcomlem  9768  ackbij1lem16  10303  div2subd  12120  symg2bas  19434  psgndiflemA  21642  evl1expd  22370  evls1maplmhm  22402  oftpos  22479  restopn2  23206  tsmsxp  24184  blcld  24539  cnllycmp  25007  dvlipcn  26053  tanregt0  26599  ostthlem1  27689  nosupbnd1lem1  27771  nosupbnd2  27779  noinfbnd1lem1  27786  noinfbnd2  27794  ax5seglem6  28967  axcontlem4  29000  axcontlem7  29003  wwlksnextwrd  29930  drngidlhash  33427  rhmpreimaprmidl  33444  qsdrngilem  33487  rsprprmprmidlb  33516  rprmirredb  33525  dfufd2lem  33542  lindsunlem  33637  lactlmhm  33647  pnfneige0  33897  qqhval2  33928  esumcocn  34044  carsgmon  34279  bnj1125  34968  heiborlem8  37778  2atjm  39402  1cvrat  39433  lvolnlelln  39541  lvolnlelpln  39542  4atlem3  39553  lplncvrlvol  39573  dalem39  39668  cdleme4a  40196  cdleme15  40235  cdleme16c  40237  cdleme19b  40261  cdleme19e  40264  cdleme20d  40269  cdleme20g  40272  cdleme20j  40275  cdleme20k  40276  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme27cl  40323  cdlemefr27cl  40360  mpaaeu  43107