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  7091  finexdc  7092  dcfi  7180  difinfsn  7299  nnnninfeq2  7328  nninfisol  7332  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  suplocexprlemru  7939  suplocsrlemb  8026  suplocsrlem  8028  aptap  8830  supinfneg  9829  infsupneg  9830  xaddf  10079  xaddval  10080  nn0ltexp2  10972  hashunlem  11068  swrdccatin1  11307  reuccatpfxs1  11329  xrmaxiflemcl  11807  xrmaxiflemlub  11810  xrmaxltsup  11820  sumeq2  11921  fsumconst  12017  prodeq2  12120  fprodconst  12183  nninfctlemfo  12613  prdsval  13358  sgrpidmndm  13505  mhmmnd  13705  ghmcmn  13916  issrg  13981  cncnp  14957  neitx  14995  dedekindeulemlu  15348  suplociccreex  15351  dedekindicclemlu  15357  cnplimclemr  15396  limccnp2cntop  15404  logbgcd1irrap  15697  lgsval  15736  usgr1vr  16102  pw1ndom3  16610