Theorem simprl3 1217

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

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

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  poxp3  8130  ttrcltr  9707  pwfseqlem5  10654  icodiamlt  15379  issubc3  17798  pgpfac1lem5  19991  clsconn  23256  txlly  23462  txnlly  23463  itg2add  25611  ftc1a  25894  nosupprefixmo  27549  noinfprefixmo  27550  nosupbnd2  27565  noinfbnd2  27580  mulsprop  27946  f1otrg  28591  ax5seglem6  28661  axcontlem10  28700  numclwwlk5  30110  locfinref  33310  btwnouttr2  35489  btwnconn1lem13  35566  midofsegid  35571  outsideofeq  35597  ivthALT  35710  mpaaeu  42381  dfsalgen2  45542