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  8102  ttrcltr  9637  pwfseqlem5  10586  icodiamlt  15373  issubc3  17785  pgpfac1lem5  20022  clsconn  23386  txlly  23592  txnlly  23593  itg2add  25728  ftc1a  26012  nosupprefixmo  27680  noinfprefixmo  27681  nosupbnd2  27696  noinfbnd2  27711  mulsprop  28138  bdayfinbndlem1  28475  f1otrg  28955  ax5seglem6  29019  axcontlem10  29058  numclwwlk5  30475  locfinref  34018  btwnouttr2  36235  btwnconn1lem13  36312  midofsegid  36317  outsideofeq  36343  ivthALT  36548  mpaaeu  43504  dfsalgen2  46696  grtrimap  48305