Theorem simprl3 1222

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

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

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 1089

This theorem is referenced by:  poxp3  8100  ttrcltr  9637  pwfseqlem5  10586  icodiamlt  15400  issubc3  17816  pgpfac1lem5  20056  clsconn  23395  txlly  23601  txnlly  23602  itg2add  25726  ftc1a  26004  nosupprefixmo  27664  noinfprefixmo  27665  nosupbnd2  27680  noinfbnd2  27695  mulsprop  28122  bdayfinbndlem1  28459  f1otrg  28939  ax5seglem6  29003  axcontlem10  29042  numclwwlk5  30458  locfinref  33985  btwnouttr2  36204  btwnconn1lem13  36281  midofsegid  36286  outsideofeq  36312  ivthALT  36517  mpaaeu  43578  dfsalgen2  46769  grtrimap  48424