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  4497  fidceq  7177  fidifsnen  7178  en2eqpr  7220  iunfidisj  7266  fdcf1  7322  ordiso2  7382  addlocpr  7910  aptiprlemu  8014  xltadd1  10295  xlesubadd  10302  icoshftf1o  10410  fztri3or  10460  elfzonelfzo  10665  exp3val  10999  nn0ltexp2  11169  hashun  11267  swrdclg  11444  subcn2  12102  divalglemeuneg  12715  dvdslegcd  12766  lcmledvds  12873  rpdvds  12902  cncongr2  12907  qexpz  13160  iuncld  15374  iscnp4  15477  cnpnei  15478  cnconst2  15492  cnpdis  15501  txcn  15534  blssps  15686  blss  15687  metcnp3  15770  metcnp  15771  lgsfcl2  16363  lgsdir  16392  lgsne0  16395  eulerpathum  16960