Theorem simpll3 1041

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

Assertion

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

Proof of Theorem simpll3

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

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

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 983

This theorem is referenced by:  frirrg  4402  fidceq  6978  fidifsnen  6979  en2eqpr  7016  iunfidisj  7060  ordiso2  7149  addlocpr  7662  aptiprlemu  7766  xltadd1  10011  xlesubadd  10018  icoshftf1o  10126  fztri3or  10174  elfzonelfzo  10372  exp3val  10699  nn0ltexp2  10867  hashun  10963  swrdclg  11117  subcn2  11672  divalglemeuneg  12284  dvdslegcd  12335  lcmledvds  12442  rpdvds  12471  cncongr2  12476  qexpz  12725  iuncld  14637  iscnp4  14740  cnpnei  14741  cnconst2  14755  cnpdis  14764  txcn  14797  blssps  14949  blss  14950  metcnp3  15033  metcnp  15034  lgsfcl2  15533  lgsdir  15562  lgsne0  15565