Theorem simprl2 1221

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  poxp2  8087  poxp3  8094  icodiamlt  15365  issubc3  17777  clsconn  23378  txlly  23584  txnlly  23585  itg2add  25720  ftc1a  26004  nosupprefixmo  27672  noinfprefixmo  27673  nosupbnd2  27688  noinfbnd2  27703  mulsprop  28112  bdayfinbndlem1  28446  f1otrg  28926  ax5seglem6  28990  axcontlem9  29028  axcontlem10  29029  clwwlkf  30105  locfinref  33979  erdszelem7  35372  btwnconn1lem13  36274  dfsalgen2  46621  grtrimap  48230  pgn4cyclex  48408