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  10085  icodiamlt  14795  issubc3  17119  pgpfac1lem5  19201  clsconn  22038  txlly  22244  txnlly  22245  itg2add  24360  ftc1a  24634  f1otrg  26657  ax5seglem6  26720  axcontlem10  26759  numclwwlk5  28167  locfinref  31105  noprefixmo  33202  nosupbnd2  33216  btwnouttr2  33483  btwnconn1lem13  33560  midofsegid  33565  outsideofeq  33591  ivthALT  33683  mpaaeu  39770  dfsalgen2  42644