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  8149  ttrcltr  9730  pwfseqlem5  10677  icodiamlt  15454  issubc3  17862  pgpfac1lem5  20062  clsconn  23368  txlly  23574  txnlly  23575  itg2add  25712  ftc1a  25996  nosupprefixmo  27664  noinfprefixmo  27665  nosupbnd2  27680  noinfbnd2  27695  mulsprop  28085  f1otrg  28850  ax5seglem6  28913  axcontlem10  28952  numclwwlk5  30369  locfinref  33872  btwnouttr2  36040  btwnconn1lem13  36117  midofsegid  36122  outsideofeq  36148  ivthALT  36353  mpaaeu  43174  dfsalgen2  46370  grtrimap  47960