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  7161  finexdc  7162  fissfi  7218  dcfi  7270  difinfsn  7393  nnnninfeq2  7422  nninfisol  7426  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  suplocexprlemru  8039  suplocsrlemb  8126  suplocsrlem  8128  aptap  8929  supinfneg  9933  infsupneg  9934  xaddf  10183  xaddval  10184  nn0ltexp2  11079  hashunlem  11176  swrdccatin1  11425  reuccatpfxs1  11447  xrmaxiflemcl  11938  xrmaxiflemlub  11941  xrmaxltsup  11951  sumeq2  12052  fsumconst  12148  prodeq2  12251  fprodconst  12314  nninfctlemfo  12744  prdsval  13507  sgrpidmndm  13654  mhmmnd  13854  ghmcmn  14065  issrg  14130  cncnp  15144  neitx  15182  dedekindeulemlu  15535  suplociccreex  15538  dedekindicclemlu  15544  cnplimclemr  15583  limccnp2cntop  15591  logbgcd1irrap  15884  lgsval  15926  usgr1vr  16292  pw1ndom3  16813