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  10156  lsmcv  21108  nllyrest  23442  axcontlem4  29052  eqlkr  39469  athgt  39826  llncvrlpln2  39927  4atlem11b  39978  2lnat  40154  cdlemblem  40163  pclfinN  40270  lhp2at0nle  40405  4atexlemex6  40444  cdlemd2  40569  cdlemd8  40575  cdleme15a  40644  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme20h  40686  cdleme21c  40697  cdleme21ct  40699  cdleme22cN  40712  cdleme23b  40720  cdleme26fALTN  40732  cdleme26f  40733  cdleme26f2ALTN  40734  cdleme26f2  40735  cdleme32le  40817  cdleme35f  40824  cdlemf1  40931  trlord  40939  cdlemg7aN  40995  cdlemg33c0  41072  trlcone  41098  cdlemg44  41103  cdlemg48  41107  cdlemky  41296  cdlemk11ta  41299  cdleml4N  41349  dihmeetlem3N  41675  dihmeetlem13N  41689  mapdpglem32  42075  baerlem3lem2  42080  baerlem5alem2  42081  baerlem5blem2  42082  mzpcong  43323  iscnrm3rlem8  49300