Theorem simp12r 1306

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp12r	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1219	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1151	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:  ackbij1lem16  10293  lsmcv  21399  nllyrest  23785  axcontlem4  29527  eqlkr  40124  athgt  40481  llncvrlpln2  40582  4atlem11b  40633  2lnat  40809  cdlemblem  40818  pclfinN  40925  lhp2at0nle  41060  4atexlemex6  41099  cdlemd2  41224  cdlemd8  41230  cdleme15a  41299  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme20h  41341  cdleme21c  41352  cdleme21ct  41354  cdleme22cN  41367  cdleme23b  41375  cdleme26fALTN  41387  cdleme26f  41388  cdleme26f2ALTN  41389  cdleme26f2  41390  cdleme32le  41472  cdleme35f  41479  cdlemf1  41586  trlord  41594  cdlemg7aN  41650  cdlemg33c0  41727  trlcone  41753  cdlemg44  41758  cdlemg48  41762  cdlemky  41951  cdlemk11ta  41954  cdleml4N  42004  dihmeetlem3N  42330  dihmeetlem13N  42344  mapdpglem32  42730  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  mzpcong  43932  iscnrm3rlem8  49999