Theorem simpll1 1020

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

Assertion

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

Proof of Theorem simpll1

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

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

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 964

This theorem is referenced by:  fidifsnen  6764  ordiso2  6920  ctssdc  6998  addlocpr  7344  xltadd1  9659  hashun  10551  fimaxq  10573  xrmaxltsup  11027  dvdslegcd  11653  lcmledvds  11751  divgcdcoprm0  11782  rpexp  11831  iscnp4  12387  cnconst2  12402  blssps  12596  blss  12597  metcnp  12681  addcncntoplem  12720  cdivcncfap  12756