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  14574  neitx  14612  dedekindeulemlu  14965  suplociccreex  14968  dedekindicclemlu  14974  cnplimclemr  15013  limccnp2cntop  15021  logbgcd1irrap  15314  lgsval  15353