Theorem simprl2 1220

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 1137	. 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:  poxp2  8068  poxp3  8075  icodiamlt  15337  issubc3  17748  clsconn  23338  txlly  23544  txnlly  23545  itg2add  25680  ftc1a  25964  nosupprefixmo  27632  noinfprefixmo  27633  nosupbnd2  27648  noinfbnd2  27663  mulsprop  28062  f1otrg  28842  ax5seglem6  28905  axcontlem9  28943  axcontlem10  28944  clwwlkf  30017  locfinref  33844  erdszelem7  35209  btwnconn1lem13  36112  dfsalgen2  46358  grtrimap  47958  pgn4cyclex  48136