Theorem simp-4r 542

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 534	. 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  544  fimax2gtri  6896  finexdc  6897  dcfi  6975  difinfsn  7094  nnnninfeq2  7122  nninfisol  7126  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  suplocexprlemru  7713  suplocsrlemb  7800  suplocsrlem  7802  aptap  8601  supinfneg  9589  infsupneg  9590  xaddf  9838  xaddval  9839  nn0ltexp2  10681  hashunlem  10775  xrmaxiflemcl  11244  xrmaxiflemlub  11247  xrmaxltsup  11257  sumeq2  11358  fsumconst  11453  prodeq2  11556  fprodconst  11619  sgrpidmndm  12751  mhmmnd  12908  issrg  13048  cncnp  13512  neitx  13550  dedekindeulemlu  13881  suplociccreex  13884  dedekindicclemlu  13890  cnplimclemr  13920  limccnp2cntop  13928  logbgcd1irrap  14170  lgsval  14187