Theorem simpll3 1064

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

Assertion

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

Proof of Theorem simpll3

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

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

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 1006

This theorem is referenced by:  frirrg  4447  fidceq  7056  fidifsnen  7057  en2eqpr  7099  iunfidisj  7145  ordiso2  7234  addlocpr  7756  aptiprlemu  7860  xltadd1  10111  xlesubadd  10118  icoshftf1o  10226  fztri3or  10274  elfzonelfzo  10476  exp3val  10804  nn0ltexp2  10972  hashun  11069  swrdclg  11235  subcn2  11876  divalglemeuneg  12489  dvdslegcd  12540  lcmledvds  12647  rpdvds  12676  cncongr2  12681  qexpz  12930  iuncld  14845  iscnp4  14948  cnpnei  14949  cnconst2  14963  cnpdis  14972  txcn  15005  blssps  15157  blss  15158  metcnp3  15241  metcnp  15242  lgsfcl2  15741  lgsdir  15770  lgsne0  15773  eulerpathum  16338