Theorem simp1l2 1264

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

Assertion

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

Proof of Theorem simp1l2

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  mapxpen  8667  lsmcv  19906  pmatcollpw2  21383  btwnconn1lem4  33664  linethru  33727  hlrelat3  36708  cvrval3  36709  cvrval4N  36710  2atlt  36735  atbtwnex  36744  1cvratlt  36770  atcvrlln2  36815  atcvrlln  36816  2llnmat  36820  lvolnlelpln  36881  lnjatN  37076  lncmp  37079  cdlemd9  37502  dihord5b  38555  dihmeetALTN  38623  mapdrvallem2  38941  itschlc0xyqsol  45181