Theorem simpll3 1040

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

Assertion

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

Proof of Theorem simpll3

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

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

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 982

This theorem is referenced by:  frirrg  4385  fidceq  6930  fidifsnen  6931  en2eqpr  6968  iunfidisj  7012  ordiso2  7101  addlocpr  7603  aptiprlemu  7707  xltadd1  9951  xlesubadd  9958  icoshftf1o  10066  fztri3or  10114  elfzonelfzo  10306  exp3val  10633  nn0ltexp2  10801  hashun  10897  subcn2  11476  divalglemeuneg  12088  dvdslegcd  12131  lcmledvds  12238  rpdvds  12267  cncongr2  12272  qexpz  12521  iuncld  14351  iscnp4  14454  cnpnei  14455  cnconst2  14469  cnpdis  14478  txcn  14511  blssps  14663  blss  14664  metcnp3  14747  metcnp  14748  lgsfcl2  15247  lgsdir  15276  lgsne0  15279