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  6971  finexdc  6972  dcfi  7056  difinfsn  7175  nnnninfeq2  7204  nninfisol  7208  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  suplocexprlemru  7805  suplocsrlemb  7892  suplocsrlem  7894  aptap  8696  supinfneg  9688  infsupneg  9689  xaddf  9938  xaddval  9939  nn0ltexp2  10820  hashunlem  10915  xrmaxiflemcl  11429  xrmaxiflemlub  11432  xrmaxltsup  11442  sumeq2  11543  fsumconst  11638  prodeq2  11741  fprodconst  11804  nninfctlemfo  12234  prdsval  12977  sgrpidmndm  13124  mhmmnd  13324  ghmcmn  13535  issrg  13599  cncnp  14552  neitx  14590  dedekindeulemlu  14943  suplociccreex  14946  dedekindicclemlu  14952  cnplimclemr  14991  limccnp2cntop  14999  logbgcd1irrap  15292  lgsval  15331