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  4470  fidceq  7123  fidifsnen  7124  en2eqpr  7166  iunfidisj  7212  ordiso2  7325  addlocpr  7850  aptiprlemu  7954  xltadd1  10208  xlesubadd  10215  icoshftf1o  10323  fztri3or  10372  elfzonelfzo  10574  exp3val  10902  nn0ltexp2  11070  hashun  11167  swrdclg  11338  subcn2  11992  divalglemeuneg  12605  dvdslegcd  12656  lcmledvds  12763  rpdvds  12792  cncongr2  12797  qexpz  13046  iuncld  14972  iscnp4  15075  cnpnei  15076  cnconst2  15090  cnpdis  15099  txcn  15132  blssps  15284  blss  15285  metcnp3  15368  metcnp  15369  lgsfcl2  15871  lgsdir  15900  lgsne0  15903  eulerpathum  16468