Theorem simprl3 1221

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8074  ttrcltr  9600  pwfseqlem5  10545  icodiamlt  15332  issubc3  17743  pgpfac1lem5  19947  clsconn  23299  txlly  23505  txnlly  23506  itg2add  25641  ftc1a  25925  nosupprefixmo  27593  noinfprefixmo  27594  nosupbnd2  27609  noinfbnd2  27624  mulsprop  28023  f1otrg  28803  ax5seglem6  28866  axcontlem10  28905  numclwwlk5  30319  locfinref  33822  btwnouttr2  36013  btwnconn1lem13  36090  midofsegid  36095  outsideofeq  36121  ivthALT  36326  mpaaeu  43140  dfsalgen2  46336  grtrimap  47946