Theorem simpll1 1026

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

Assertion

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

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 990	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	adantr 274	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  fidifsnen  6832  ordiso2  6996  ctssdc  7074  addlocpr  7473  xltadd1  9808  nn0ltexp2  10619  hashun  10714  fimaxq  10736  xrmaxltsup  11195  dvdslegcd  11893  lcmledvds  11998  divgcdcoprm0  12029  rpexp  12081  qexpz  12278  iscnp4  12818  cnconst2  12833  blssps  13027  blss  13028  metcnp  13112  addcncntoplem  13151  cdivcncfap  13187  lgsfvalg  13506  lgsmod  13527  lgsdir  13536  lgsne0  13539