Theorem simprl3 1217

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  pwfseqlem5  10136  icodiamlt  14856  issubc3  17191  pgpfac1lem5  19282  clsconn  22143  txlly  22349  txnlly  22350  itg2add  24472  ftc1a  24749  f1otrg  26777  ax5seglem6  26840  axcontlem10  26879  numclwwlk5  28285  locfinref  31324  nosupprefixmo  33500  noinfprefixmo  33501  nosupbnd2  33516  noinfbnd2  33531  btwnouttr2  33907  btwnconn1lem13  33984  midofsegid  33989  outsideofeq  34015  ivthALT  34107  mpaaeu  40502  dfsalgen2  43382