Theorem simpll3 1069

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

Assertion

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

Proof of Theorem simpll3

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  frirrg  4495  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ordiso2  7375  addlocpr  7903  aptiprlemu  8007  xltadd1  10280  xlesubadd  10287  icoshftf1o  10395  fztri3or  10445  elfzonelfzo  10650  exp3val  10980  nn0ltexp2  11149  hashun  11247  swrdclg  11424  subcn2  12079  divalglemeuneg  12692  dvdslegcd  12743  lcmledvds  12850  rpdvds  12879  cncongr2  12884  qexpz  13133  iuncld  15218  iscnp4  15321  cnpnei  15322  cnconst2  15336  cnpdis  15345  txcn  15378  blssps  15530  blss  15531  metcnp3  15614  metcnp  15615  lgsfcl2  16137  lgsdir  16166  lgsne0  16169  eulerpathum  16734