Theorem simprl2 1226

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprl2	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprl2

Step	Hyp	Ref	Expression
1		simp2 1143	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 734	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  poxp3  8097  icodiamlt  15398  issubc3  17814  clsconn  23420  txlly  23626  txnlly  23627  itg2add  25751  ftc1a  26029  nosupprefixmo  27689  noinfprefixmo  27690  nosupbnd2  27705  noinfbnd2  27720  mulsprop  28147  bdayfinbndlem1  28484  f1otrg  28964  ax5seglem6  29028  axcontlem9  29066  axcontlem10  29067  clwwlkf  30142  locfinref  34032  erdszelem7  35432  btwnconn1lem13  36334  dfsalgen2  46791  grtrimap  48446  pgn4cyclex  48624