Theorem simprl3 1216

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pwfseqlem5  10087  icodiamlt  14797  issubc3  17121  pgpfac1lem5  19203  clsconn  22040  txlly  22246  txnlly  22247  itg2add  24362  ftc1a  24636  f1otrg  26659  ax5seglem6  26722  axcontlem10  26761  numclwwlk5  28169  locfinref  31107  noprefixmo  33204  nosupbnd2  33218  btwnouttr2  33485  btwnconn1lem13  33562  midofsegid  33567  outsideofeq  33593  ivthALT  33685  mpaaeu  39757  dfsalgen2  42631