Theorem simpll3 1062

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

Assertion

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

Proof of Theorem simpll3

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

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

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 1004

This theorem is referenced by:  frirrg  4438  fidceq  7019  fidifsnen  7020  en2eqpr  7057  iunfidisj  7101  ordiso2  7190  addlocpr  7711  aptiprlemu  7815  xltadd1  10060  xlesubadd  10067  icoshftf1o  10175  fztri3or  10223  elfzonelfzo  10423  exp3val  10750  nn0ltexp2  10918  hashun  11014  swrdclg  11168  subcn2  11808  divalglemeuneg  12420  dvdslegcd  12471  lcmledvds  12578  rpdvds  12607  cncongr2  12612  qexpz  12861  iuncld  14774  iscnp4  14877  cnpnei  14878  cnconst2  14892  cnpdis  14901  txcn  14934  blssps  15086  blss  15087  metcnp3  15170  metcnp  15171  lgsfcl2  15670  lgsdir  15699  lgsne0  15702