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  6899  ordiso2  7065  ctssdc  7143  addlocpr  7566  xltadd1  9908  nn0ltexp2  10724  hashun  10820  fimaxq  10842  xrmaxltsup  11301  dvdslegcd  12000  lcmledvds  12105  divgcdcoprm0  12136  rpexp  12188  qexpz  12387  dfgrp3mlem  13057  rhmdvdsr  13542  rnglidlmcl  13813  iscnp4  14195  cnconst2  14210  blssps  14404  blss  14405  metcnp  14489  addcncntoplem  14528  cdivcncfap  14564  lgsfvalg  14884  lgsmod  14905  lgsdir  14914  lgsne0  14917