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  7077  finexdc  7078  dcfi  7164  difinfsn  7283  nnnninfeq2  7312  nninfisol  7316  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  suplocexprlemru  7922  suplocsrlemb  8009  suplocsrlem  8011  aptap  8813  supinfneg  9807  infsupneg  9808  xaddf  10057  xaddval  10058  nn0ltexp2  10948  hashunlem  11043  swrdccatin1  11278  reuccatpfxs1  11300  xrmaxiflemcl  11777  xrmaxiflemlub  11780  xrmaxltsup  11790  sumeq2  11891  fsumconst  11986  prodeq2  12089  fprodconst  12152  nninfctlemfo  12582  prdsval  13327  sgrpidmndm  13474  mhmmnd  13674  ghmcmn  13885  issrg  13949  cncnp  14925  neitx  14963  dedekindeulemlu  15316  suplociccreex  15319  dedekindicclemlu  15325  cnplimclemr  15364  limccnp2cntop  15372  logbgcd1irrap  15665  lgsval  15704  usgr1vr  16067  pw1ndom3  16467