Theorem simp-4r 544

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 536	. 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  546  fimax2gtri  7096  finexdc  7097  dcfi  7185  difinfsn  7304  nnnninfeq2  7333  nninfisol  7337  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  suplocexprlemru  7944  suplocsrlemb  8031  suplocsrlem  8033  aptap  8835  supinfneg  9834  infsupneg  9835  xaddf  10084  xaddval  10085  nn0ltexp2  10977  hashunlem  11073  swrdccatin1  11315  reuccatpfxs1  11337  xrmaxiflemcl  11828  xrmaxiflemlub  11831  xrmaxltsup  11841  sumeq2  11942  fsumconst  12038  prodeq2  12141  fprodconst  12204  nninfctlemfo  12634  prdsval  13379  sgrpidmndm  13526  mhmmnd  13726  ghmcmn  13937  issrg  14002  cncnp  14983  neitx  15021  dedekindeulemlu  15374  suplociccreex  15377  dedekindicclemlu  15383  cnplimclemr  15422  limccnp2cntop  15430  logbgcd1irrap  15723  lgsval  15762  usgr1vr  16128  pw1ndom3  16649