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  8148  ttrcltr  9688  pwfseqlem5  10659  icodiamlt  15509  issubc3  17924  pgpfac1lem5  20175  clsconn  23617  txlly  23824  txnlly  23825  itg2add  25949  ftc1a  26227  nosupprefixmo  27895  noinfprefixmo  27896  nosupbnd2  27911  noinfbnd2  27926  mulsprop  28354  bdayfinbndlem1  28691  f1otrg  29251  ax5seglem6  29315  axcontlem10  29354  numclwwlk5  30786  locfinref  34271  btwnouttr2  36527  btwnconn1lem13  36604  midofsegid  36609  outsideofeq  36635  ivthALT  36879  mpaaeu  43910  dfsalgen2  47088  grtrimap  48746