Theorem simpll1 1039

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

Assertion

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

Proof of Theorem simpll1

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  fidifsnen  6979  ordiso2  7149  ctssdc  7227  addlocpr  7662  xltadd1  10011  nn0ltexp2  10867  hashun  10963  fimaxq  10985  xrmaxltsup  11619  dvdslegcd  12335  lcmledvds  12442  divgcdcoprm0  12473  rpexp  12525  qexpz  12725  dfgrp3mlem  13480  rhmdvdsr  13987  rnglidlmcl  14292  iscnp4  14740  cnconst2  14755  blssps  14949  blss  14950  metcnp  15034  addcncntoplem  15083  cdivcncfap  15126  lgsfvalg  15532  lgsmod  15553  lgsdir  15562  lgsne0  15565