Theorem simp1l1 1365

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

Assertion

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

Proof of Theorem simp1l1

Step	Hyp	Ref	Expression
1		simpl1 1242	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1163	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1107

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 198  df-an 385  df-3an 1109

This theorem is referenced by:  mapxpen  8332  lsmcv  19413  archiabl  30133  trisegint  32510  linethru  32635  hlrelat3  35300  cvrval3  35301  cvrval4N  35302  2atlt  35327  atbtwnex  35336  1cvratlt  35362  atcvrlln2  35407  atcvrlln  35408  2llnmat  35412  lplnexllnN  35452  lvolnlelpln  35473  lnjatN  35668  lncvrat  35670  lncmp  35671  cdlemd9  36094  dihord5b  37147  dihmeetALTN  37215  dih1dimatlem0  37216  mapdrvallem2  37533