Theorem simp-4r 531

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 523	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 274	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-5r  533  fimax2gtri  6788  finexdc  6789  difinfsn  6978  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  suplocexprlemru  7520  suplocsrlemb  7607  suplocsrlem  7609  supinfneg  9383  infsupneg  9384  xaddf  9620  xaddval  9621  hashunlem  10543  xrmaxiflemcl  11007  xrmaxiflemlub  11010  xrmaxltsup  11020  sumeq2  11121  fsumconst  11216  prodeq2  11319  cncnp  12388  neitx  12426  dedekindeulemlu  12757  suplociccreex  12760  dedekindicclemlu  12766  cnplimclemr  12796  limccnp2cntop  12804