Theorem simp-4r 544

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

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

Syntax hints:   → wi 4   ∧ wa 104

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 is referenced by:  simp-5r  546  fimax2gtri  7158  finexdc  7159  fissfi  7215  dcfi  7267  difinfsn  7390  nnnninfeq2  7419  nninfisol  7423  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  suplocexprlemru  8030  suplocsrlemb  8117  suplocsrlem  8119  aptap  8920  supinfneg  9923  infsupneg  9924  xaddf  10173  xaddval  10174  nn0ltexp2  11067  hashunlem  11163  swrdccatin1  11410  reuccatpfxs1  11432  xrmaxiflemcl  11923  xrmaxiflemlub  11926  xrmaxltsup  11936  sumeq2  12037  fsumconst  12133  prodeq2  12236  fprodconst  12299  nninfctlemfo  12729  prdsval  13475  sgrpidmndm  13622  mhmmnd  13822  ghmcmn  14033  issrg  14098  cncnp  15082  neitx  15120  dedekindeulemlu  15473  suplociccreex  15476  dedekindicclemlu  15482  cnplimclemr  15521  limccnp2cntop  15529  logbgcd1irrap  15822  lgsval  15864  usgr1vr  16230  pw1ndom3  16751