Theorem simpll1 1063

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

Assertion

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

Proof of Theorem simpll1

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

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

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 1007

This theorem is referenced by:  fidifsnen  7100  ordiso2  7277  ctssdc  7355  addlocpr  7799  xltadd1  10154  nn0ltexp2  11015  hashun  11112  fimaxq  11135  xrmaxltsup  11879  dvdslegcd  12596  lcmledvds  12703  divgcdcoprm0  12734  rpexp  12786  qexpz  12986  dfgrp3mlem  13742  rhmdvdsr  14251  rnglidlmcl  14556  iscnp4  15009  cnconst2  15024  blssps  15218  blss  15219  metcnp  15303  addcncntoplem  15352  cdivcncfap  15395  lgsfvalg  15804  lgsmod  15825  lgsdir  15834  lgsne0  15837  clwwlknonex2  16360  eulerpathum  16402