Theorem simp12r 1289

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1202	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1134	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:  ackbij1lem16  10147  lsmcv  21131  nllyrest  23461  axcontlem4  29050  eqlkr  39559  athgt  39916  llncvrlpln2  40017  4atlem11b  40068  2lnat  40244  cdlemblem  40253  pclfinN  40360  lhp2at0nle  40495  4atexlemex6  40534  cdlemd2  40659  cdlemd8  40665  cdleme15a  40734  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme20h  40776  cdleme21c  40787  cdleme21ct  40789  cdleme22cN  40802  cdleme23b  40810  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme32le  40907  cdleme35f  40914  cdlemf1  41021  trlord  41029  cdlemg7aN  41085  cdlemg33c0  41162  trlcone  41188  cdlemg44  41193  cdlemg48  41197  cdlemky  41386  cdlemk11ta  41389  cdleml4N  41439  dihmeetlem3N  41765  dihmeetlem13N  41779  mapdpglem32  42165  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  mzpcong  43418  iscnrm3rlem8  49434