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  7052  ordiso2  7228  ctssdc  7306  addlocpr  7749  xltadd1  10104  nn0ltexp2  10964  hashun  11061  fimaxq  11084  xrmaxltsup  11812  dvdslegcd  12528  lcmledvds  12635  divgcdcoprm0  12666  rpexp  12718  qexpz  12918  dfgrp3mlem  13674  rhmdvdsr  14182  rnglidlmcl  14487  iscnp4  14935  cnconst2  14950  blssps  15144  blss  15145  metcnp  15229  addcncntoplem  15278  cdivcncfap  15321  lgsfvalg  15727  lgsmod  15748  lgsdir  15757  lgsne0  15760  clwwlknonex2  16248