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  7020  ordiso2  7190  ctssdc  7268  addlocpr  7711  xltadd1  10060  nn0ltexp2  10918  hashun  11014  fimaxq  11036  xrmaxltsup  11755  dvdslegcd  12471  lcmledvds  12578  divgcdcoprm0  12609  rpexp  12661  qexpz  12861  dfgrp3mlem  13617  rhmdvdsr  14124  rnglidlmcl  14429  iscnp4  14877  cnconst2  14892  blssps  15086  blss  15087  metcnp  15171  addcncntoplem  15220  cdivcncfap  15263  lgsfvalg  15669  lgsmod  15690  lgsdir  15699  lgsne0  15702