Theorem simpll3 1065

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

Assertion

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

Proof of Theorem simpll3

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

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

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 1007

This theorem is referenced by:  frirrg  4453  fidceq  7099  fidifsnen  7100  en2eqpr  7142  iunfidisj  7188  ordiso2  7277  addlocpr  7799  aptiprlemu  7903  xltadd1  10154  xlesubadd  10161  icoshftf1o  10269  fztri3or  10317  elfzonelfzo  10519  exp3val  10847  nn0ltexp2  11015  hashun  11112  swrdclg  11278  subcn2  11932  divalglemeuneg  12545  dvdslegcd  12596  lcmledvds  12703  rpdvds  12732  cncongr2  12737  qexpz  12986  iuncld  14906  iscnp4  15009  cnpnei  15010  cnconst2  15024  cnpdis  15033  txcn  15066  blssps  15218  blss  15219  metcnp3  15302  metcnp  15303  lgsfcl2  15805  lgsdir  15834  lgsne0  15837  eulerpathum  16402