Theorem simprl3 1233

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  poxp3  8124  ttrcltr  9665  pwfseqlem5  10615  icodiamlt  15456  issubc3  17873  pgpfac1lem5  20112  clsconn  23478  txlly  23684  txnlly  23685  itg2add  25809  ftc1a  26087  nosupprefixmo  27752  noinfprefixmo  27753  nosupbnd2  27768  noinfbnd2  27783  mulsprop  28211  bdayfinbndlem1  28548  f1otrg  29028  ax5seglem6  29092  axcontlem10  29131  numclwwlk5  30547  locfinref  34099  btwnouttr2  36333  btwnconn1lem13  36410  midofsegid  36415  outsideofeq  36441  ivthALT  36656  mpaaeu  43688  dfsalgen2  46876  grtrimap  48531