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  7086  finexdc  7087  dcfi  7174  difinfsn  7293  nnnninfeq2  7322  nninfisol  7326  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  suplocexprlemru  7932  suplocsrlemb  8019  suplocsrlem  8021  aptap  8823  supinfneg  9822  infsupneg  9823  xaddf  10072  xaddval  10073  nn0ltexp2  10964  hashunlem  11060  swrdccatin1  11299  reuccatpfxs1  11321  xrmaxiflemcl  11799  xrmaxiflemlub  11802  xrmaxltsup  11812  sumeq2  11913  fsumconst  12008  prodeq2  12111  fprodconst  12174  nninfctlemfo  12604  prdsval  13349  sgrpidmndm  13496  mhmmnd  13696  ghmcmn  13907  issrg  13971  cncnp  14947  neitx  14985  dedekindeulemlu  15338  suplociccreex  15341  dedekindicclemlu  15347  cnplimclemr  15386  limccnp2cntop  15394  logbgcd1irrap  15687  lgsval  15726  usgr1vr  16092  pw1ndom3  16539