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  8187  poxp3  8194  icodiamlt  15634  issubc3  18053  clsconn  23778  txlly  23985  txnlly  23986  itg2add  26110  ftc1a  26387  nosupprefixmo  28087  noinfprefixmo  28088  nosupbnd2  28103  noinfbnd2  28118  mulsprop  28546  bdayfinbndlem1  28883  f1otrg  29478  ax5seglem6  29542  axcontlem9  29580  axcontlem10  29581  clwwlkf  30668  locfinref  34543  erdszelem7  36129  btwnconn1lem13  37042  dfsalgen2  47556  grtrimap  49251  pgn4cyclex  49429