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  6929  finexdc  6930  dcfi  7010  difinfsn  7129  nnnninfeq2  7157  nninfisol  7161  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  suplocexprlemru  7748  suplocsrlemb  7835  suplocsrlem  7837  aptap  8637  supinfneg  9625  infsupneg  9626  xaddf  9874  xaddval  9875  nn0ltexp2  10721  hashunlem  10816  xrmaxiflemcl  11285  xrmaxiflemlub  11288  xrmaxltsup  11298  sumeq2  11399  fsumconst  11494  prodeq2  11597  fprodconst  11660  sgrpidmndm  12881  mhmmnd  13058  ghmcmn  13265  issrg  13319  cncnp  14187  neitx  14225  dedekindeulemlu  14556  suplociccreex  14559  dedekindicclemlu  14565  cnplimclemr  14595  limccnp2cntop  14603  logbgcd1irrap  14845  lgsval  14863