Theorem simp1l2 1265

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

Assertion

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

Proof of Theorem simp1l2

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  mapxpen  8879  lsmcv  20318  pmatcollpw2  21835  sltlpss  34014  btwnconn1lem4  34319  linethru  34382  hlrelat3  37353  cvrval3  37354  cvrval4N  37355  2atlt  37380  atbtwnex  37389  1cvratlt  37415  atcvrlln2  37460  atcvrlln  37461  2llnmat  37465  lvolnlelpln  37526  lnjatN  37721  lncmp  37724  cdlemd9  38147  dihord5b  39200  dihmeetALTN  39268  mapdrvallem2  39586  itschlc0xyqsol  46001