Theorem simp12r 1288

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  ackbij1lem16  10230  lsmcv  20754  nllyrest  22990  axcontlem4  28256  eqlkr  38017  athgt  38375  llncvrlpln2  38476  4atlem11b  38527  2lnat  38703  cdlemblem  38712  pclfinN  38819  lhp2at0nle  38954  4atexlemex6  38993  cdlemd2  39118  cdlemd8  39124  cdleme15a  39193  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme20h  39235  cdleme21c  39246  cdleme21ct  39248  cdleme22cN  39261  cdleme23b  39269  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme32le  39366  cdleme35f  39373  cdlemf1  39480  trlord  39488  cdlemg7aN  39544  cdlemg33c0  39621  trlcone  39647  cdlemg44  39652  cdlemg48  39656  cdlemky  39845  cdlemk11ta  39848  cdleml4N  39898  dihmeetlem3N  40224  dihmeetlem13N  40238  mapdpglem32  40624  baerlem3lem2  40629  baerlem5alem2  40630  baerlem5blem2  40631  mzpcong  41759  iscnrm3rlem8  47628