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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

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

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 1011

This theorem is referenced by:  frirrg  4493  fidceq  7165  fidifsnen  7166  en2eqpr  7208  iunfidisj  7254  fdcf1  7310  ordiso2  7369  addlocpr  7897  aptiprlemu  8001  xltadd1  10261  xlesubadd  10268  icoshftf1o  10376  fztri3or  10426  elfzonelfzo  10631  exp3val  10961  nn0ltexp2  11130  hashun  11228  swrdclg  11405  subcn2  12060  divalglemeuneg  12673  dvdslegcd  12724  lcmledvds  12831  rpdvds  12860  cncongr2  12865  qexpz  13114  iuncld  15199  iscnp4  15302  cnpnei  15303  cnconst2  15317  cnpdis  15326  txcn  15359  blssps  15511  blss  15512  metcnp3  15595  metcnp  15596  lgsfcl2  16108  lgsdir  16137  lgsne0  16140  eulerpathum  16705