Theorem simp1l1 1267

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

Assertion

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

Proof of Theorem simp1l1

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

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

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 1088

This theorem is referenced by:  poxp3  8089  mapxpen  9067  hash7g  14400  lsmcv  21087  sltlpss  27873  archiabl  33208  trisegint  36144  linethru  36269  hlrelat3  39584  cvrval3  39585  cvrval4N  39586  2atlt  39611  atbtwnex  39620  1cvratlt  39646  atcvrlln2  39691  atcvrlln  39692  2llnmat  39696  lplnexllnN  39736  lvolnlelpln  39757  lnjatN  39952  lncvrat  39954  lncmp  39955  cdlemd9  40378  dihord5b  41431  dihmeetALTN  41499  dih1dimatlem0  41500  mapdrvallem2  41817  grumnudlem  44442