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  7050  ordiso2  7223  ctssdc  7301  addlocpr  7744  xltadd1  10099  nn0ltexp2  10959  hashun  11055  fimaxq  11078  xrmaxltsup  11806  dvdslegcd  12522  lcmledvds  12629  divgcdcoprm0  12660  rpexp  12712  qexpz  12912  dfgrp3mlem  13668  rhmdvdsr  14176  rnglidlmcl  14481  iscnp4  14929  cnconst2  14944  blssps  15138  blss  15139  metcnp  15223  addcncntoplem  15272  cdivcncfap  15315  lgsfvalg  15721  lgsmod  15742  lgsdir  15751  lgsne0  15754  clwwlknonex2  16224