Theorem simprl3 1227

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp3  8090  ttrcltr  9628  pwfseqlem5  10577  icodiamlt  15391  issubc3  17807  pgpfac1lem5  20047  clsconn  23413  txlly  23619  txnlly  23620  itg2add  25744  ftc1a  26022  nosupprefixmo  27682  noinfprefixmo  27683  nosupbnd2  27698  noinfbnd2  27713  mulsprop  28140  bdayfinbndlem1  28477  f1otrg  28957  ax5seglem6  29021  axcontlem10  29060  numclwwlk5  30476  locfinref  34025  btwnouttr2  36250  btwnconn1lem13  36327  midofsegid  36332  outsideofeq  36358  ivthALT  36563  mpaaeu  43595  dfsalgen2  46784  grtrimap  48439