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  4445  fidceq  7051  fidifsnen  7052  en2eqpr  7094  iunfidisj  7139  ordiso2  7228  addlocpr  7749  aptiprlemu  7853  xltadd1  10104  xlesubadd  10111  icoshftf1o  10219  fztri3or  10267  elfzonelfzo  10468  exp3val  10796  nn0ltexp2  10964  hashun  11061  swrdclg  11224  subcn2  11865  divalglemeuneg  12477  dvdslegcd  12528  lcmledvds  12635  rpdvds  12664  cncongr2  12669  qexpz  12918  iuncld  14832  iscnp4  14935  cnpnei  14936  cnconst2  14950  cnpdis  14959  txcn  14992  blssps  15144  blss  15145  metcnp3  15228  metcnp  15229  lgsfcl2  15728  lgsdir  15757  lgsne0  15760