Theorem simprl3 1218

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 724	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  ttrcltr  9435  pwfseqlem5  10403  icodiamlt  15128  issubc3  17545  pgpfac1lem5  19663  clsconn  22562  txlly  22768  txnlly  22769  itg2add  24905  ftc1a  25182  f1otrg  27213  ax5seglem6  27283  axcontlem10  27322  numclwwlk5  28731  locfinref  31770  nosupprefixmo  33882  noinfprefixmo  33883  nosupbnd2  33898  noinfbnd2  33913  btwnouttr2  34303  btwnconn1lem13  34380  midofsegid  34385  outsideofeq  34411  ivthALT  34503  mpaaeu  40955  dfsalgen2  43834