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  8155  mapxpen  9141  lsmcv  21302  pmatcollpw2  22972  ltslpss  28138  btwnconn1lem4  36603  linethru  36666  hlrelat3  40227  cvrval3  40228  cvrval4N  40229  2atlt  40254  atbtwnex  40263  1cvratlt  40289  atcvrlln2  40334  atcvrlln  40335  2llnmat  40339  lvolnlelpln  40400  lnjatN  40595  lncmp  40598  cdlemd9  41021  dihord5b  42074  dihmeetALTN  42142  mapdrvallem2  42460  itschlc0xyqsol  49588