Theorem simpll3 1065

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

Assertion

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

Proof of Theorem simpll3

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  frirrg  4476  fidceq  7137  fidifsnen  7138  en2eqpr  7180  iunfidisj  7226  ordiso2  7339  addlocpr  7867  aptiprlemu  7971  xltadd1  10231  xlesubadd  10238  icoshftf1o  10346  fztri3or  10396  elfzonelfzo  10600  exp3val  10930  nn0ltexp2  11099  hashun  11197  swrdclg  11370  subcn2  12025  divalglemeuneg  12638  dvdslegcd  12689  lcmledvds  12796  rpdvds  12825  cncongr2  12830  qexpz  13079  iuncld  15110  iscnp4  15213  cnpnei  15214  cnconst2  15228  cnpdis  15237  txcn  15270  blssps  15422  blss  15423  metcnp3  15506  metcnp  15507  lgsfcl2  16009  lgsdir  16038  lgsne0  16041  eulerpathum  16606