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  8132  ttrcltr  9676  pwfseqlem5  10623  icodiamlt  15411  issubc3  17818  pgpfac1lem5  20018  clsconn  23324  txlly  23530  txnlly  23531  itg2add  25667  ftc1a  25951  nosupprefixmo  27619  noinfprefixmo  27620  nosupbnd2  27635  noinfbnd2  27650  mulsprop  28040  f1otrg  28805  ax5seglem6  28868  axcontlem10  28907  numclwwlk5  30324  locfinref  33838  btwnouttr2  36017  btwnconn1lem13  36094  midofsegid  36099  outsideofeq  36125  ivthALT  36330  mpaaeu  43146  dfsalgen2  46346  grtrimap  47951