Theorem simpll3 1033

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

Assertion

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

Proof of Theorem simpll3

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  frirrg  4333  fidceq  6843  fidifsnen  6844  en2eqpr  6881  iunfidisj  6919  ordiso2  7008  addlocpr  7485  aptiprlemu  7589  xltadd1  9820  xlesubadd  9827  icoshftf1o  9935  fztri3or  9982  elfzonelfzo  10173  exp3val  10465  nn0ltexp2  10631  hashun  10727  subcn2  11261  divalglemeuneg  11869  dvdslegcd  11906  lcmledvds  12011  rpdvds  12040  cncongr2  12045  qexpz  12291  iuncld  12868  iscnp4  12971  cnpnei  12972  cnconst2  12986  cnpdis  12995  txcn  13028  blssps  13180  blss  13181  metcnp3  13264  metcnp  13265  lgsfcl2  13660  lgsdir  13689  lgsne0  13692