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  6903  finexdc  6904  dcfi  6982  difinfsn  7101  nnnninfeq2  7129  nninfisol  7133  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  suplocexprlemru  7720  suplocsrlemb  7807  suplocsrlem  7809  aptap  8609  supinfneg  9597  infsupneg  9598  xaddf  9846  xaddval  9847  nn0ltexp2  10691  hashunlem  10786  xrmaxiflemcl  11255  xrmaxiflemlub  11258  xrmaxltsup  11268  sumeq2  11369  fsumconst  11464  prodeq2  11567  fprodconst  11630  sgrpidmndm  12826  mhmmnd  12985  issrg  13153  cncnp  13769  neitx  13807  dedekindeulemlu  14138  suplociccreex  14141  dedekindicclemlu  14147  cnplimclemr  14177  limccnp2cntop  14185  logbgcd1irrap  14427  lgsval  14444