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  7172  finexdc  7173  fissfi  7229  dcfi  7281  difinfsn  7404  nnnninfeq2  7433  nninfisol  7437  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  suplocexprlemru  8050  suplocsrlemb  8137  suplocsrlem  8139  aptap  8942  supinfneg  9948  infsupneg  9949  xaddf  10199  xaddval  10200  nn0ltexp2  11099  hashunlem  11196  swrdccatin1  11445  reuccatpfxs1  11467  xrmaxiflemcl  11958  xrmaxiflemlub  11961  xrmaxltsup  11971  sumeq2  12072  fsumconst  12168  prodeq2  12271  fprodconst  12334  nninfctlemfo  12764  sgrpidmndm  13684  mhmmnd  13872  ghmcmn  14083  prdsval  14118  issrg  14211  cncnp  15224  neitx  15262  dedekindeulemlu  15615  suplociccreex  15618  dedekindicclemlu  15624  cnplimclemr  15663  limccnp2cntop  15671  logbgcd1irrap  15964  lgsval  16006  usgr1vr  16372  pw1ndom3  16903