Theorem simpll3 1062

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

Assertion

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

Proof of Theorem simpll3

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

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

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 1004

This theorem is referenced by:  frirrg  4441  fidceq  7039  fidifsnen  7040  en2eqpr  7077  iunfidisj  7121  ordiso2  7210  addlocpr  7731  aptiprlemu  7835  xltadd1  10080  xlesubadd  10087  icoshftf1o  10195  fztri3or  10243  elfzonelfzo  10444  exp3val  10771  nn0ltexp2  10939  hashun  11035  swrdclg  11190  subcn2  11830  divalglemeuneg  12442  dvdslegcd  12493  lcmledvds  12600  rpdvds  12629  cncongr2  12634  qexpz  12883  iuncld  14797  iscnp4  14900  cnpnei  14901  cnconst2  14915  cnpdis  14924  txcn  14957  blssps  15109  blss  15110  metcnp3  15193  metcnp  15194  lgsfcl2  15693  lgsdir  15722  lgsne0  15725