Theorem simprl3 1239

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprl3	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprl3

Step	Hyp	Ref	Expression
1		simp3 1156	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 741	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8173  ttrcltr  9724  pwfseqlem5  10755  icodiamlt  15614  issubc3  18033  pgpfac1lem5  20304  clsconn  23757  txlly  23964  txnlly  23965  itg2add  26089  ftc1a  26366  nosupprefixmo  28066  noinfprefixmo  28067  nosupbnd2  28082  noinfbnd2  28097  mulsprop  28525  bdayfinbndlem1  28862  f1otrg  29457  ax5seglem6  29521  axcontlem10  29560  numclwwlk5  30998  locfinref  34523  btwnouttr2  36883  btwnconn1lem13  36960  midofsegid  36965  outsideofeq  36991  ivthALT  37219  mpaaeu  44261  dfsalgen2  47459  grtrimap  49154