Theorem simpll1 1067

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

Assertion

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

Proof of Theorem simpll1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidifsnen  7172  ordiso2  7376  ctssdc  7454  addlocpr  7904  xltadd1  10289  nn0ltexp2  11162  hashun  11260  fimaxq  11285  xrmaxltsup  12042  dvdslegcd  12759  lcmledvds  12866  divgcdcoprm0  12897  rpexp  12950  qexpz  13153  dfgrp3mlem  13954  gsumconstcmn  14217  rhmdvdsr  14533  rnglidlmcl  14868  iscnp4  15371  cnconst2  15386  blssps  15580  blss  15581  metcnp  15665  addcncntoplem  15714  cdivcncfap  15757  lgsfvalg  16246  lgsmod  16267  lgsdir  16276  lgsne0  16279  clwwlknonex2  16802  eulerpathum  16844