Theorem simprl3 1239

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8155  ttrcltr  9695  pwfseqlem5  10666  icodiamlt  15515  issubc3  17931  pgpfac1lem5  20176  clsconn  23617  txlly  23823  txnlly  23824  itg2add  25948  ftc1a  26226  nosupprefixmo  27894  noinfprefixmo  27895  nosupbnd2  27910  noinfbnd2  27925  mulsprop  28353  bdayfinbndlem1  28690  f1otrg  29250  ax5seglem6  29314  axcontlem10  29353  numclwwlk5  30769  locfinref  34255  btwnouttr2  36527  btwnconn1lem13  36604  midofsegid  36609  outsideofeq  36635  ivthALT  36879  mpaaeu  43910  dfsalgen2  47088  grtrimap  48746