Theorem simp1l2 1351

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

Assertion

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

Proof of Theorem simp1l2

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 383  df-3an 1073

This theorem is referenced by:  mapxpen  8282  lsmcv  19355  pmatcollpw2  20803  btwnconn1lem4  32534  linethru  32597  hlrelat3  35220  cvrval3  35221  cvrval4N  35222  2atlt  35247  atbtwnex  35256  1cvratlt  35282  atcvrlln2  35327  atcvrlln  35328  2llnmat  35332  lvolnlelpln  35393  lnjatN  35588  lncmp  35591  cdlemd9  36015  dihord5b  37069  dihmeetALTN  37137  mapdrvallem2  37455