Theorem simprl2 1236

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 1153	. 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:  poxp2  8127  poxp3  8134  icodiamlt  15479  issubc3  17896  clsconn  23548  txlly  23754  txnlly  23755  itg2add  25879  ftc1a  26157  nosupprefixmo  27822  noinfprefixmo  27823  nosupbnd2  27838  noinfbnd2  27853  mulsprop  28281  bdayfinbndlem1  28618  f1otrg  29129  ax5seglem6  29193  axcontlem9  29231  axcontlem10  29232  clwwlkf  30307  locfinref  34148  erdszelem7  35560  btwnconn1lem13  36462  dfsalgen2  46913  grtrimap  48568  pgn4cyclex  48746