Theorem simp-4r 548

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 540	. 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  550  fimax2gtri  7200  finexdc  7201  fissfi  7257  dcfi  7309  difinfsn  7434  nnnninfeq2  7463  nninfisol  7467  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  suplocexprlemru  8080  suplocsrlemb  8167  suplocsrlem  8169  aptap  8972  supinfneg  9978  infsupneg  9979  xaddf  10229  xaddval  10230  nn0ltexp2  11130  hashunlem  11227  swrdccatin1  11480  reuccatpfxs1  11502  xrmaxiflemcl  11994  xrmaxiflemlub  11997  xrmaxltsup  12007  sumeq2  12108  fsumconst  12204  prodeq2  12307  fprodconst  12370  nninfctlemfo  12800  sgrpidmndm  13716  mhmmnd  13902  ghmcmn  14114  prdsval  14156  issrg  14252  cncnp  15314  neitx  15352  dedekindeulemlu  15705  suplociccreex  15708  dedekindicclemlu  15714  cnplimclemr  15753  limccnp2cntop  15761  logbgcd1irrap  16055  lgsval  16106  usgr1vr  16472  pw1ndom3  17003