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  8160  ttrcltr  9710  pwfseqlem5  10741  icodiamlt  15598  issubc3  18017  pgpfac1lem5  20288  clsconn  23741  txlly  23948  txnlly  23949  itg2add  26073  ftc1a  26350  nosupprefixmo  28050  noinfprefixmo  28051  nosupbnd2  28066  noinfbnd2  28081  mulsprop  28509  bdayfinbndlem1  28846  f1otrg  29441  ax5seglem6  29505  axcontlem10  29544  numclwwlk5  30982  locfinref  34466  btwnouttr2  36767  btwnconn1lem13  36844  midofsegid  36849  outsideofeq  36875  ivthALT  37103  mpaaeu  44136  dfsalgen2  47320  grtrimap  49015