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  7211  finexdc  7212  fissfi  7268  dcfi  7321  difinfsn  7447  nnnninfeq2  7476  nninfisol  7480  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  suplocexprlemru  8093  suplocsrlemb  8180  suplocsrlem  8182  aptap  8987  supinfneg  10012  infsupneg  10013  xaddf  10264  xaddval  10265  nn0ltexp2  11170  hashunlem  11267  swrdccatin1  11520  reuccatpfxs1  11542  xrmaxiflemcl  12037  xrmaxiflemlub  12040  xrmaxltsup  12050  sumeq2  12151  fsumconst  12247  prodeq2  12350  fprodconst  12413  nninfctlemfo  12843  sgrpidmndm  13793  mhmmnd  13979  ghmcmn  14222  prdsval  14281  issrg  14377  psrbaglefifi  15177  cncnp  15468  neitx  15506  dedekindeulemlu  15859  suplociccreex  15862  dedekindicclemlu  15868  cnplimclemr  15907  limccnp2cntop  15915  logbgcd1irrap  16218  lgsval  16340  usgr1vr  16706  pw1ndom3  17237