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  4386  fidceq  6939  fidifsnen  6940  en2eqpr  6977  iunfidisj  7021  ordiso2  7110  addlocpr  7622  aptiprlemu  7726  xltadd1  9970  xlesubadd  9977  icoshftf1o  10085  fztri3or  10133  elfzonelfzo  10325  exp3val  10652  nn0ltexp2  10820  hashun  10916  subcn2  11495  divalglemeuneg  12107  dvdslegcd  12158  lcmledvds  12265  rpdvds  12294  cncongr2  12299  qexpz  12548  iuncld  14459  iscnp4  14562  cnpnei  14563  cnconst2  14577  cnpdis  14586  txcn  14619  blssps  14771  blss  14772  metcnp3  14855  metcnp  14856  lgsfcl2  15355  lgsdir  15384  lgsne0  15387