Theorem simpll1 1062

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

Assertion

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

Proof of Theorem simpll1

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

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

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 1006

This theorem is referenced by:  fidifsnen  7057  ordiso2  7234  ctssdc  7312  addlocpr  7756  xltadd1  10111  nn0ltexp2  10972  hashun  11069  fimaxq  11092  xrmaxltsup  11823  dvdslegcd  12540  lcmledvds  12647  divgcdcoprm0  12678  rpexp  12730  qexpz  12930  dfgrp3mlem  13686  rhmdvdsr  14195  rnglidlmcl  14500  iscnp4  14948  cnconst2  14963  blssps  15157  blss  15158  metcnp  15242  addcncntoplem  15291  cdivcncfap  15334  lgsfvalg  15740  lgsmod  15761  lgsdir  15770  lgsne0  15773  clwwlknonex2  16296  eulerpathum  16338