Theorem simp1l2 1280

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

Assertion

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

Proof of Theorem simp1l2

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  poxp3  8123  mapxpen  9108  lsmcv  21198  pmatcollpw2  22825  ltslpss  27988  btwnconn1lem4  36400  linethru  36463  hlrelat3  39996  cvrval3  39997  cvrval4N  39998  2atlt  40023  atbtwnex  40032  1cvratlt  40058  atcvrlln2  40103  atcvrlln  40104  2llnmat  40108  lvolnlelpln  40169  lnjatN  40364  lncmp  40367  cdlemd9  40790  dihord5b  41843  dihmeetALTN  41911  mapdrvallem2  42229  itschlc0xyqsol  49349