Theorem syl23anc 1404

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  suppofss1d  8222  suppofss2d  8223  cnfcomlem  9701  ackbij1lem16  10313  div2subd  12144  symg2bas  19608  rhmpreimaprmidl  21636  psgndiflemA  21908  evl1expd  22664  evls1maplmhm  22696  oftpos  22768  restopn2  23496  tsmsxp  24475  blcld  24825  cnllycmp  25278  dvlipcn  26315  tanregt0  26868  ostthlem1  27955  nosupbnd1lem1  28066  nosupbnd2  28074  noinfbnd1lem1  28081  noinfbnd2  28089  angmgmaddov1  29389  ax5seglem6  29513  axcontlem4  29546  axcontlem7  29549  wwlksnextwrd  30487  drngidlhash  33984  qsdrngilem  34019  rsprprmprmidlb  34056  rprmirredb  34065  dfufd2lem  34082  lindsunlem  34257  lactlmhm  34267  pnfneige0  34584  qqhval2  34615  esumcocn  34713  carsgmon  34947  bnj1125  35623  heiborlem8  38754  2atjm  40504  1cvrat  40535  lvolnlelln  40643  lvolnlelpln  40644  4atlem3  40655  lplncvrlvol  40675  dalem39  40770  cdleme4a  41298  cdleme15  41337  cdleme16c  41339  cdleme19b  41363  cdleme19e  41366  cdleme20d  41371  cdleme20g  41374  cdleme20j  41377  cdleme20k  41378  cdleme20l2  41380  cdleme20l  41381  cdleme20m  41382  cdleme22e  41403  cdleme22eALTN  41404  cdleme22f  41405  cdleme27cl  41425  cdlemefr27cl  41462  mpaaeu  44153