Theorem simp1l2 1153

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

Assertion

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

Proof of Theorem simp1l2

Step	Hyp	Ref	Expression
1		simpl2 1063	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1080	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  mapxpen  8070  lsmcv  19060  pmatcollpw2  20502  btwnconn1lem4  31836  linethru  31899  hlrelat3  34175  cvrval3  34176  cvrval4N  34177  2atlt  34202  atbtwnex  34211  1cvratlt  34237  atcvrlln2  34282  atcvrlln  34283  2llnmat  34287  lvolnlelpln  34348  lnjatN  34543  lncmp  34546  cdlemd9  34970  dihord5b  36025  dihmeetALTN  36093  mapdrvallem2  36411