Theorem simprl3 1222

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp3  8093  ttrcltr  9628  pwfseqlem5  10577  icodiamlt  15391  issubc3  17807  pgpfac1lem5  20047  clsconn  23405  txlly  23611  txnlly  23612  itg2add  25736  ftc1a  26014  nosupprefixmo  27678  noinfprefixmo  27679  nosupbnd2  27694  noinfbnd2  27709  mulsprop  28136  bdayfinbndlem1  28473  f1otrg  28953  ax5seglem6  29017  axcontlem10  29056  numclwwlk5  30473  locfinref  34001  btwnouttr2  36220  btwnconn1lem13  36297  midofsegid  36302  outsideofeq  36328  ivthALT  36533  mpaaeu  43596  dfsalgen2  46787  grtrimap  48436