Theorem simp-4r 537

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-5r  539  fimax2gtri  6875  finexdc  6876  dcfi  6954  difinfsn  7073  nnnninfeq2  7101  nninfisol  7105  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  suplocexprlemru  7668  suplocsrlemb  7755  suplocsrlem  7757  supinfneg  9541  infsupneg  9542  xaddf  9788  xaddval  9789  nn0ltexp2  10631  hashunlem  10726  xrmaxiflemcl  11195  xrmaxiflemlub  11198  xrmaxltsup  11208  sumeq2  11309  fsumconst  11404  prodeq2  11507  fprodconst  11570  sgrpidmndm  12643  cncnp  12983  neitx  13021  dedekindeulemlu  13352  suplociccreex  13355  dedekindicclemlu  13361  cnplimclemr  13391  limccnp2cntop  13399  logbgcd1irrap  13641  lgsval  13658