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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  poxp3  8147  mapxpen  9132  lsmcv  21246  pmatcollpw2  22916  ltslpss  28082  btwnconn1lem4  36563  linethru  36626  hlrelat3  40167  cvrval3  40168  cvrval4N  40169  2atlt  40194  atbtwnex  40203  1cvratlt  40229  atcvrlln2  40274  atcvrlln  40275  2llnmat  40279  lvolnlelpln  40340  lnjatN  40535  lncmp  40538  cdlemd9  40961  dihord5b  42014  dihmeetALTN  42082  mapdrvallem2  42400  itschlc0xyqsol  49530