Theorem simpll1 1067

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

Assertion

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

Proof of Theorem simpll1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidifsnen  7178  ordiso2  7382  ctssdc  7460  addlocpr  7910  xltadd1  10295  nn0ltexp2  11169  hashun  11267  fimaxq  11292  xrmaxltsup  12049  dvdslegcd  12766  lcmledvds  12873  divgcdcoprm0  12904  rpexp  12957  qexpz  13160  dfgrp3mlem  13962  gsumconstcmn  14266  rhmdvdsr  14591  rnglidlmcl  14926  iscnp4  15477  cnconst2  15492  blssps  15686  blss  15687  metcnp  15771  addcncntoplem  15820  cdivcncfap  15863  lgsfvalg  16362  lgsmod  16383  lgsdir  16392  lgsne0  16395  clwwlknonex2  16918  eulerpathum  16960