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  8160  mapxpen  9155  lsmcv  21412  pmatcollpw2  23089  ltslpss  28287  btwnconn1lem4  36835  linethru  36898  hlrelat3  40449  cvrval3  40450  cvrval4N  40451  2atlt  40476  atbtwnex  40485  1cvratlt  40511  atcvrlln2  40556  atcvrlln  40557  2llnmat  40561  lvolnlelpln  40622  lnjatN  40817  lncmp  40820  cdlemd9  41243  dihord5b  42296  dihmeetALTN  42364  mapdrvallem2  42682  itschlc0xyqsol  49848