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  8075  ttrcltr  9601  pwfseqlem5  10549  icodiamlt  15340  issubc3  17751  pgpfac1lem5  19988  clsconn  23340  txlly  23546  txnlly  23547  itg2add  25682  ftc1a  25966  nosupprefixmo  27634  noinfprefixmo  27635  nosupbnd2  27650  noinfbnd2  27665  mulsprop  28064  f1otrg  28844  ax5seglem6  28907  axcontlem10  28946  numclwwlk5  30360  locfinref  33846  btwnouttr2  36056  btwnconn1lem13  36133  midofsegid  36138  outsideofeq  36164  ivthALT  36369  mpaaeu  43183  dfsalgen2  46379  grtrimap  47979