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  8102  mapxpen  9083  hash7g  14421  lsmcv  21108  ltslpss  27916  archiabl  33292  trisegint  36244  linethru  36369  hlrelat3  39788  cvrval3  39789  cvrval4N  39790  2atlt  39815  atbtwnex  39824  1cvratlt  39850  atcvrlln2  39895  atcvrlln  39896  2llnmat  39900  lplnexllnN  39940  lvolnlelpln  39961  lnjatN  40156  lncvrat  40158  lncmp  40159  cdlemd9  40582  dihord5b  41635  dihmeetALTN  41703  dih1dimatlem0  41704  mapdrvallem2  42021  grumnudlem  44641