Theorem simprl3 1239

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  poxp3  8142  ttrcltr  9681  pwfseqlem5  10643  icodiamlt  15485  issubc3  17901  pgpfac1lem5  20146  clsconn  23587  txlly  23793  txnlly  23794  itg2add  25918  ftc1a  26196  nosupprefixmo  27864  noinfprefixmo  27865  nosupbnd2  27880  noinfbnd2  27895  mulsprop  28323  bdayfinbndlem1  28660  f1otrg  29220  ax5seglem6  29284  axcontlem10  29323  numclwwlk5  30739  locfinref  34231  btwnouttr2  36514  btwnconn1lem13  36591  midofsegid  36596  outsideofeq  36622  ivthALT  36846  mpaaeu  43877  dfsalgen2  47055  grtrimap  48713