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  7031  finexdc  7032  dcfi  7116  difinfsn  7235  nnnninfeq2  7264  nninfisol  7268  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  suplocexprlemru  7874  suplocsrlemb  7961  suplocsrlem  7963  aptap  8765  supinfneg  9758  infsupneg  9759  xaddf  10008  xaddval  10009  nn0ltexp2  10898  hashunlem  10993  swrdccatin1  11223  reuccatpfxs1  11245  xrmaxiflemcl  11722  xrmaxiflemlub  11725  xrmaxltsup  11735  sumeq2  11836  fsumconst  11931  prodeq2  12034  fprodconst  12097  nninfctlemfo  12527  prdsval  13272  sgrpidmndm  13419  mhmmnd  13619  ghmcmn  13830  issrg  13894  cncnp  14869  neitx  14907  dedekindeulemlu  15260  suplociccreex  15263  dedekindicclemlu  15269  cnplimclemr  15308  limccnp2cntop  15316  logbgcd1irrap  15609  lgsval  15648