Theorem simpll1 1038

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

Assertion

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

Proof of Theorem simpll1

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

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

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 982

This theorem is referenced by:  fidifsnen  6940  ordiso2  7110  ctssdc  7188  addlocpr  7622  xltadd1  9970  nn0ltexp2  10820  hashun  10916  fimaxq  10938  xrmaxltsup  11442  dvdslegcd  12158  lcmledvds  12265  divgcdcoprm0  12296  rpexp  12348  qexpz  12548  dfgrp3mlem  13302  rhmdvdsr  13809  rnglidlmcl  14114  iscnp4  14562  cnconst2  14577  blssps  14771  blss  14772  metcnp  14856  addcncntoplem  14905  cdivcncfap  14948  lgsfvalg  15354  lgsmod  15375  lgsdir  15384  lgsne0  15387