Theorem simpll1 1021

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

Assertion

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

Proof of Theorem simpll1

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

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

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 965

This theorem is referenced by:  fidifsnen  6772  ordiso2  6928  ctssdc  7006  addlocpr  7368  xltadd1  9689  hashun  10583  fimaxq  10605  xrmaxltsup  11059  dvdslegcd  11689  lcmledvds  11787  divgcdcoprm0  11818  rpexp  11867  iscnp4  12426  cnconst2  12441  blssps  12635  blss  12636  metcnp  12720  addcncntoplem  12759  cdivcncfap  12795