Theorem simpll1 1036

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

Assertion

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

Proof of Theorem simpll1

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

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

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 980

This theorem is referenced by:  fidifsnen  6869  ordiso2  7033  ctssdc  7111  addlocpr  7534  xltadd1  9875  nn0ltexp2  10688  hashun  10784  fimaxq  10806  xrmaxltsup  11265  dvdslegcd  11964  lcmledvds  12069  divgcdcoprm0  12100  rpexp  12152  qexpz  12349  dfgrp3mlem  12967  iscnp4  13688  cnconst2  13703  blssps  13897  blss  13898  metcnp  13982  addcncntoplem  14021  cdivcncfap  14057  lgsfvalg  14376  lgsmod  14397  lgsdir  14406  lgsne0  14409