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  9695  pwfseqlem5  10672  icodiamlt  15525  issubc3  17938  pgpfac1lem5  20208  clsconn  23655  txlly  23862  txnlly  23863  itg2add  25987  ftc1a  26264  nosupprefixmo  27936  noinfprefixmo  27937  nosupbnd2  27952  noinfbnd2  27967  mulsprop  28395  bdayfinbndlem1  28732  f1otrg  29327  ax5seglem6  29391  axcontlem10  29430  numclwwlk5  30868  locfinref  34351  btwnouttr2  36602  btwnconn1lem13  36679  midofsegid  36684  outsideofeq  36710  ivthALT  36954  mpaaeu  43991  dfsalgen2  47169  grtrimap  48864