Theorem simp1l1 1263

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  poxp3  8155  mapxpen  9168  lsmcv  21041  sltlpss  27879  archiabl  32998  trisegint  35755  linethru  35880  hlrelat3  39015  cvrval3  39016  cvrval4N  39017  2atlt  39042  atbtwnex  39051  1cvratlt  39077  atcvrlln2  39122  atcvrlln  39123  2llnmat  39127  lplnexllnN  39167  lvolnlelpln  39188  lnjatN  39383  lncvrat  39385  lncmp  39386  cdlemd9  39809  dihord5b  40862  dihmeetALTN  40930  dih1dimatlem0  40931  mapdrvallem2  41248  grumnudlem  43864