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  6962  finexdc  6963  dcfi  7047  difinfsn  7166  nnnninfeq2  7195  nninfisol  7199  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  suplocexprlemru  7786  suplocsrlemb  7873  suplocsrlem  7875  aptap  8677  supinfneg  9669  infsupneg  9670  xaddf  9919  xaddval  9920  nn0ltexp2  10801  hashunlem  10896  xrmaxiflemcl  11410  xrmaxiflemlub  11413  xrmaxltsup  11423  sumeq2  11524  fsumconst  11619  prodeq2  11722  fprodconst  11785  nninfctlemfo  12207  sgrpidmndm  13061  mhmmnd  13246  ghmcmn  13457  issrg  13521  cncnp  14466  neitx  14504  dedekindeulemlu  14857  suplociccreex  14860  dedekindicclemlu  14866  cnplimclemr  14905  limccnp2cntop  14913  logbgcd1irrap  15206  lgsval  15245