Theorem simp1l1 1268

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

Assertion

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

Proof of Theorem simp1l1

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp3  8093  mapxpen  9074  hash7g  14439  lsmcv  21131  ltslpss  27914  archiabl  33274  trisegint  36226  linethru  36351  hlrelat3  39872  cvrval3  39873  cvrval4N  39874  2atlt  39899  atbtwnex  39908  1cvratlt  39934  atcvrlln2  39979  atcvrlln  39980  2llnmat  39984  lplnexllnN  40024  lvolnlelpln  40045  lnjatN  40240  lncvrat  40242  lncmp  40243  cdlemd9  40666  dihord5b  41719  dihmeetALTN  41787  dih1dimatlem0  41788  mapdrvallem2  42105  grumnudlem  44730