Theorem simprl2 1238

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8162  poxp3  8169  icodiamlt  15610  issubc3  18029  clsconn  23753  txlly  23960  txnlly  23961  itg2add  26085  ftc1a  26362  nosupprefixmo  28062  noinfprefixmo  28063  nosupbnd2  28078  noinfbnd2  28093  mulsprop  28521  bdayfinbndlem1  28858  f1otrg  29453  ax5seglem6  29517  axcontlem9  29555  axcontlem10  29556  clwwlkf  30643  locfinref  34519  erdszelem7  36048  btwnconn1lem13  36956  dfsalgen2  47444  grtrimap  49139  pgn4cyclex  49317