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  8092  ttrcltr  9625  pwfseqlem5  10574  icodiamlt  15361  issubc3  17773  pgpfac1lem5  20010  clsconn  23374  txlly  23580  txnlly  23581  itg2add  25716  ftc1a  26000  nosupprefixmo  27668  noinfprefixmo  27669  nosupbnd2  27684  noinfbnd2  27699  mulsprop  28126  bdayfinbndlem1  28463  f1otrg  28943  ax5seglem6  29007  axcontlem10  29046  numclwwlk5  30463  locfinref  33998  btwnouttr2  36216  btwnconn1lem13  36293  midofsegid  36298  outsideofeq  36324  ivthALT  36529  mpaaeu  43392  dfsalgen2  46585  grtrimap  48194