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  7005  finexdc  7006  dcfi  7090  difinfsn  7209  nnnninfeq2  7238  nninfisol  7242  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  suplocexprlemru  7839  suplocsrlemb  7926  suplocsrlem  7928  aptap  8730  supinfneg  9723  infsupneg  9724  xaddf  9973  xaddval  9974  nn0ltexp2  10861  hashunlem  10956  xrmaxiflemcl  11600  xrmaxiflemlub  11603  xrmaxltsup  11613  sumeq2  11714  fsumconst  11809  prodeq2  11912  fprodconst  11975  nninfctlemfo  12405  prdsval  13149  sgrpidmndm  13296  mhmmnd  13496  ghmcmn  13707  issrg  13771  cncnp  14746  neitx  14784  dedekindeulemlu  15137  suplociccreex  15140  dedekindicclemlu  15146  cnplimclemr  15185  limccnp2cntop  15193  logbgcd1irrap  15486  lgsval  15525