Theorem syl23anc 1374

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  suppofss1d  8210  suppofss2d  8211  cnfcomlem  9724  ackbij1lem16  10260  div2subd  12073  symg2bas  19359  psgndiflemA  21550  evl1expd  22289  evls1maplmhm  22321  oftpos  22398  restopn2  23125  tsmsxp  24103  blcld  24458  cnllycmp  24926  dvlipcn  25971  tanregt0  26518  ostthlem1  27605  nosupbnd1lem1  27687  nosupbnd2  27695  noinfbnd1lem1  27702  noinfbnd2  27710  ax5seglem6  28817  axcontlem4  28850  axcontlem7  28853  wwlksnextwrd  29780  drngidlhash  33246  rhmpreimaprmidl  33263  qsdrngilem  33306  rsprprmprmidlb  33335  rprmirredb  33344  dfufd2lem  33364  lindsunlem  33453  pnfneige0  33683  qqhval2  33714  esumcocn  33830  carsgmon  34065  bnj1125  34754  heiborlem8  37422  2atjm  39048  1cvrat  39079  lvolnlelln  39187  lvolnlelpln  39188  4atlem3  39199  lplncvrlvol  39219  dalem39  39314  cdleme4a  39842  cdleme15  39881  cdleme16c  39883  cdleme19b  39907  cdleme19e  39910  cdleme20d  39915  cdleme20g  39918  cdleme20j  39921  cdleme20k  39922  cdleme20l2  39924  cdleme20l  39925  cdleme20m  39926  cdleme22e  39947  cdleme22eALTN  39948  cdleme22f  39949  cdleme27cl  39969  cdlemefr27cl  40006  mpaaeu  42716