Theorem simp1l1 1283

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  poxp3  8146  mapxpen  9131  hash7g  14523  lsmcv  21243  ltslpss  28067  archiabl  33459  trisegint  36453  linethru  36578  hlrelat3  40111  cvrval3  40112  cvrval4N  40113  2atlt  40138  atbtwnex  40147  1cvratlt  40173  atcvrlln2  40218  atcvrlln  40219  2llnmat  40223  lplnexllnN  40263  lvolnlelpln  40284  lnjatN  40479  lncvrat  40481  lncmp  40482  cdlemd9  40905  dihord5b  41958  dihmeetALTN  42026  dih1dimatlem0  42027  mapdrvallem2  42344  grumnudlem  44922