Theorem simprl3 1237

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

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

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 1103

This theorem is referenced by:  poxp3  8142  ttrcltr  9681  pwfseqlem5  10644  icodiamlt  15485  issubc3  17902  pgpfac1lem5  20147  clsconn  23552  txlly  23758  txnlly  23759  itg2add  25883  ftc1a  26161  nosupprefixmo  27826  noinfprefixmo  27827  nosupbnd2  27842  noinfbnd2  27857  mulsprop  28285  bdayfinbndlem1  28622  f1otrg  29157  ax5seglem6  29221  axcontlem10  29260  numclwwlk5  30676  locfinref  34172  btwnouttr2  36409  btwnconn1lem13  36486  midofsegid  36491  outsideofeq  36517  ivthALT  36731  mpaaeu  43764  dfsalgen2  46942  grtrimap  48597