Theorem simpll3 1028

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

Assertion

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

Proof of Theorem simpll3

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

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

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 970

This theorem is referenced by:  frirrg  4328  fidceq  6835  fidifsnen  6836  en2eqpr  6873  iunfidisj  6911  ordiso2  7000  addlocpr  7477  aptiprlemu  7581  xltadd1  9812  xlesubadd  9819  icoshftf1o  9927  fztri3or  9974  elfzonelfzo  10165  exp3val  10457  nn0ltexp2  10623  hashun  10718  subcn2  11252  divalglemeuneg  11860  dvdslegcd  11897  lcmledvds  12002  rpdvds  12031  cncongr2  12036  qexpz  12282  iuncld  12755  iscnp4  12858  cnpnei  12859  cnconst2  12873  cnpdis  12882  txcn  12915  blssps  13067  blss  13068  metcnp3  13151  metcnp  13152  lgsfcl2  13547  lgsdir  13576  lgsne0  13579