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  8089  ttrcltr  9617  pwfseqlem5  10565  icodiamlt  15352  issubc3  17764  pgpfac1lem5  20001  clsconn  23365  txlly  23571  txnlly  23572  itg2add  25707  ftc1a  25991  nosupprefixmo  27659  noinfprefixmo  27660  nosupbnd2  27675  noinfbnd2  27690  mulsprop  28089  f1otrg  28869  ax5seglem6  28933  axcontlem10  28972  numclwwlk5  30389  locfinref  33926  btwnouttr2  36138  btwnconn1lem13  36215  midofsegid  36220  outsideofeq  36246  ivthALT  36451  mpaaeu  43307  dfsalgen2  46501  grtrimap  48110