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  4476  fidceq  7137  fidifsnen  7138  en2eqpr  7180  iunfidisj  7226  ordiso2  7339  addlocpr  7867  aptiprlemu  7971  xltadd1  10228  xlesubadd  10235  icoshftf1o  10343  fztri3or  10393  elfzonelfzo  10597  exp3val  10927  nn0ltexp2  11096  hashun  11194  swrdclg  11367  subcn2  12021  divalglemeuneg  12634  dvdslegcd  12685  lcmledvds  12792  rpdvds  12821  cncongr2  12826  qexpz  13075  iuncld  15092  iscnp4  15195  cnpnei  15196  cnconst2  15210  cnpdis  15219  txcn  15252  blssps  15404  blss  15405  metcnp3  15488  metcnp  15489  lgsfcl2  15991  lgsdir  16020  lgsne0  16023  eulerpathum  16588