Theorem simp12r 1286

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ackbij1lem16  9991  lsmcv  20403  nllyrest  22637  axcontlem4  27335  eqlkr  37113  athgt  37470  llncvrlpln2  37571  4atlem11b  37622  2lnat  37798  cdlemblem  37807  pclfinN  37914  lhp2at0nle  38049  4atexlemex6  38088  cdlemd2  38213  cdlemd8  38219  cdleme15a  38288  cdleme16b  38293  cdleme16c  38294  cdleme16d  38295  cdleme20h  38330  cdleme21c  38341  cdleme21ct  38343  cdleme22cN  38356  cdleme23b  38364  cdleme26fALTN  38376  cdleme26f  38377  cdleme26f2ALTN  38378  cdleme26f2  38379  cdleme32le  38461  cdleme35f  38468  cdlemf1  38575  trlord  38583  cdlemg7aN  38639  cdlemg33c0  38716  trlcone  38742  cdlemg44  38747  cdlemg48  38751  cdlemky  38940  cdlemk11ta  38943  cdleml4N  38993  dihmeetlem3N  39319  dihmeetlem13N  39333  mapdpglem32  39719  baerlem3lem2  39724  baerlem5alem2  39725  baerlem5blem2  39726  mzpcong  40794  iscnrm3rlem8  46241