Theorem simp-4r 548

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 540	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 276	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-5r  550  fimax2gtri  7206  finexdc  7207  fissfi  7263  dcfi  7315  difinfsn  7440  nnnninfeq2  7469  nninfisol  7473  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  suplocexprlemru  8086  suplocsrlemb  8173  suplocsrlem  8175  aptap  8979  supinfneg  9997  infsupneg  9998  xaddf  10248  xaddval  10249  nn0ltexp2  11149  hashunlem  11246  swrdccatin1  11499  reuccatpfxs1  11521  xrmaxiflemcl  12013  xrmaxiflemlub  12016  xrmaxltsup  12026  sumeq2  12127  fsumconst  12223  prodeq2  12326  fprodconst  12389  nninfctlemfo  12819  sgrpidmndm  13735  mhmmnd  13921  ghmcmn  14133  prdsval  14175  issrg  14271  cncnp  15333  neitx  15371  dedekindeulemlu  15724  suplociccreex  15727  dedekindicclemlu  15733  cnplimclemr  15772  limccnp2cntop  15780  logbgcd1irrap  16078  lgsval  16135  usgr1vr  16501  pw1ndom3  17032