Theorem simp1l2 1286

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

Assertion

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

Proof of Theorem simp1l2

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8171  mapxpen  9167  lsmcv  21426  pmatcollpw2  23103  ltslpss  28301  btwnconn1lem4  36949  linethru  37012  hlrelat3  40576  cvrval3  40577  cvrval4N  40578  2atlt  40603  atbtwnex  40612  1cvratlt  40638  atcvrlln2  40683  atcvrlln  40684  2llnmat  40688  lvolnlelpln  40749  lnjatN  40944  lncmp  40947  cdlemd9  41370  dihord5b  42423  dihmeetALTN  42491  mapdrvallem2  42809  itschlc0xyqsol  49986