Theorem simprl3 1220

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 398  df-3an 1089

This theorem is referenced by:  ttrcltr  9518  pwfseqlem5  10465  icodiamlt  15192  issubc3  17609  pgpfac1lem5  19727  clsconn  22626  txlly  22832  txnlly  22833  itg2add  24969  ftc1a  25246  f1otrg  27277  ax5seglem6  27347  axcontlem10  27386  numclwwlk5  28797  locfinref  31836  nosupprefixmo  33948  noinfprefixmo  33949  nosupbnd2  33964  noinfbnd2  33979  btwnouttr2  34369  btwnconn1lem13  34446  midofsegid  34451  outsideofeq  34477  ivthALT  34569  mpaaeu  41013  dfsalgen2  43929