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  8161  mapxpen  9174  lsmcv  21036  sltlpss  27853  archiabl  32927  trisegint  35657  linethru  35782  hlrelat3  38917  cvrval3  38918  cvrval4N  38919  2atlt  38944  atbtwnex  38953  1cvratlt  38979  atcvrlln2  39024  atcvrlln  39025  2llnmat  39029  lplnexllnN  39069  lvolnlelpln  39090  lnjatN  39285  lncvrat  39287  lncmp  39288  cdlemd9  39711  dihord5b  40764  dihmeetALTN  40832  dih1dimatlem0  40833  mapdrvallem2  41150  grumnudlem  43753

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »