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  7071  finexdc  7072  dcfi  7156  difinfsn  7275  nnnninfeq2  7304  nninfisol  7308  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  suplocexprlemru  7914  suplocsrlemb  8001  suplocsrlem  8003  aptap  8805  supinfneg  9798  infsupneg  9799  xaddf  10048  xaddval  10049  nn0ltexp2  10939  hashunlem  11034  swrdccatin1  11265  reuccatpfxs1  11287  xrmaxiflemcl  11764  xrmaxiflemlub  11767  xrmaxltsup  11777  sumeq2  11878  fsumconst  11973  prodeq2  12076  fprodconst  12139  nninfctlemfo  12569  prdsval  13314  sgrpidmndm  13461  mhmmnd  13661  ghmcmn  13872  issrg  13936  cncnp  14912  neitx  14950  dedekindeulemlu  15303  suplociccreex  15306  dedekindicclemlu  15312  cnplimclemr  15351  limccnp2cntop  15359  logbgcd1irrap  15652  lgsval  15691  pw1ndom3  16383