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  7176  fidifsnen  7177  en2eqpr  7219  iunfidisj  7265  fdcf1  7322  ordiso2  7382  addlocpr  7910  aptiprlemu  8014  xltadd1  10296  xlesubadd  10303  icoshftf1o  10411  fztri3or  10461  elfzonelfzo  10666  exp3val  11000  nn0ltexp2  11170  hashun  11268  swrdclg  11445  subcn2  12103  divalglemeuneg  12716  dvdslegcd  12767  lcmledvds  12874  rpdvds  12903  cncongr2  12908  qexpz  13161  iuncld  15353  iscnp4  15456  cnpnei  15457  cnconst2  15471  cnpdis  15480  txcn  15513  blssps  15665  blss  15666  metcnp3  15749  metcnp  15750  lgsfcl2  16342  lgsdir  16371  lgsne0  16374  eulerpathum  16939