Theorem simp12r 1287

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1200	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1133	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  ackbij1lem16  10256  lsmcv  21112  nllyrest  23441  axcontlem4  28913  eqlkr  39075  athgt  39433  llncvrlpln2  39534  4atlem11b  39585  2lnat  39761  cdlemblem  39770  pclfinN  39877  lhp2at0nle  40012  4atexlemex6  40051  cdlemd2  40176  cdlemd8  40182  cdleme15a  40251  cdleme16b  40256  cdleme16c  40257  cdleme16d  40258  cdleme20h  40293  cdleme21c  40304  cdleme21ct  40306  cdleme22cN  40319  cdleme23b  40327  cdleme26fALTN  40339  cdleme26f  40340  cdleme26f2ALTN  40341  cdleme26f2  40342  cdleme32le  40424  cdleme35f  40431  cdlemf1  40538  trlord  40546  cdlemg7aN  40602  cdlemg33c0  40679  trlcone  40705  cdlemg44  40710  cdlemg48  40714  cdlemky  40903  cdlemk11ta  40906  cdleml4N  40956  dihmeetlem3N  41282  dihmeetlem13N  41296  mapdpglem32  41682  baerlem3lem2  41687  baerlem5alem2  41688  baerlem5blem2  41689  mzpcong  42962  iscnrm3rlem8  48828