Theorem simpll1 1060

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

Assertion

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

Proof of Theorem simpll1

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

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

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 1004

This theorem is referenced by:  fidifsnen  7045  ordiso2  7218  ctssdc  7296  addlocpr  7739  xltadd1  10089  nn0ltexp2  10948  hashun  11044  fimaxq  11067  xrmaxltsup  11790  dvdslegcd  12506  lcmledvds  12613  divgcdcoprm0  12644  rpexp  12696  qexpz  12896  dfgrp3mlem  13652  rhmdvdsr  14160  rnglidlmcl  14465  iscnp4  14913  cnconst2  14928  blssps  15122  blss  15123  metcnp  15207  addcncntoplem  15256  cdivcncfap  15299  lgsfvalg  15705  lgsmod  15726  lgsdir  15735  lgsne0  15738