Theorem simpll3 1005

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

Assertion

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

Proof of Theorem simpll3

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 945

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  frirrg  4232  fidceq  6716  fidifsnen  6717  en2eqpr  6754  iunfidisj  6786  ordiso2  6872  addlocpr  7289  aptiprlemu  7393  xltadd1  9549  xlesubadd  9556  icoshftf1o  9664  fztri3or  9709  elfzonelfzo  9897  exp3val  10185  hashun  10441  subcn2  10969  divalglemeuneg  11465  dvdslegcd  11498  lcmledvds  11594  rpdvds  11623  cncongr2  11628  iuncld  12124  iscnp4  12226  cnpnei  12227  cnconst2  12241  cnpdis  12250  txcn  12283  blssps  12413  blss  12414  metcnp3  12497  metcnp  12498