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  8204  ttrcltr  9754  pwfseqlem5  10787  icodiamlt  15649  issubc3  18074  pgpfac1lem5  20346  clsconn  23803  txlly  24010  txnlly  24011  itg2add  26135  ftc1a  26412  nosupprefixmo  28114  noinfprefixmo  28115  nosupbnd2  28130  noinfbnd2  28145  mulsprop  28573  bdayfinbndlem1  28910  f1otrg  29505  ax5seglem6  29569  axcontlem10  29608  numclwwlk5  31046  locfinref  34584  btwnouttr2  37002  btwnconn1lem13  37079  midofsegid  37084  outsideofeq  37110  ivthALT  37338  mpaaeu  44417  dfsalgen2  47624  grtrimap  49319