Theorem simp12r 1285

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

Assertion

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

Proof of Theorem simp12r

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ackbij1lem16  9922  lsmcv  20318  nllyrest  22545  axcontlem4  27238  eqlkr  37040  athgt  37397  llncvrlpln2  37498  4atlem11b  37549  2lnat  37725  cdlemblem  37734  pclfinN  37841  lhp2at0nle  37976  4atexlemex6  38015  cdlemd2  38140  cdlemd8  38146  cdleme15a  38215  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme20h  38257  cdleme21c  38268  cdleme21ct  38270  cdleme22cN  38283  cdleme23b  38291  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme32le  38388  cdleme35f  38395  cdlemf1  38502  trlord  38510  cdlemg7aN  38566  cdlemg33c0  38643  trlcone  38669  cdlemg44  38674  cdlemg48  38678  cdlemky  38867  cdlemk11ta  38870  cdleml4N  38920  dihmeetlem3N  39246  dihmeetlem13N  39260  mapdpglem32  39646  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  mzpcong  40710  iscnrm3rlem8  46129