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  8148  mapxpen  9141  lsmcv  21328  pmatcollpw2  23003  ltslpss  28173  btwnconn1lem4  36670  linethru  36733  hlrelat3  40285  cvrval3  40286  cvrval4N  40287  2atlt  40312  atbtwnex  40321  1cvratlt  40347  atcvrlln2  40392  atcvrlln  40393  2llnmat  40397  lvolnlelpln  40458  lnjatN  40653  lncmp  40656  cdlemd9  41079  dihord5b  42132  dihmeetALTN  42200  mapdrvallem2  42518  itschlc0xyqsol  49697