Theorem simpll3 1069

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

Assertion

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

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1033	. 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  ax-ia3 108

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

This theorem is used by:  frirrg  4495  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ordiso2  7376  addlocpr  7904  aptiprlemu  8008  xltadd1  10289  xlesubadd  10296  icoshftf1o  10404  fztri3or  10454  elfzonelfzo  10659  exp3val  10992  nn0ltexp2  11162  hashun  11260  swrdclg  11437  subcn2  12095  divalglemeuneg  12708  dvdslegcd  12759  lcmledvds  12866  rpdvds  12895  cncongr2  12900  qexpz  13153  iuncld  15268  iscnp4  15371  cnpnei  15372  cnconst2  15386  cnpdis  15395  txcn  15428  blssps  15580  blss  15581  metcnp3  15664  metcnp  15665  lgsfcl2  16247  lgsdir  16276  lgsne0  16279  eulerpathum  16844