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  8095  poxp3  8102  icodiamlt  15373  issubc3  17785  clsconn  23386  txlly  23592  txnlly  23593  itg2add  25728  ftc1a  26012  nosupprefixmo  27680  noinfprefixmo  27681  nosupbnd2  27696  noinfbnd2  27711  mulsprop  28138  bdayfinbndlem1  28475  f1otrg  28955  ax5seglem6  29019  axcontlem9  29057  axcontlem10  29058  clwwlkf  30134  locfinref  34018  erdszelem7  35410  btwnconn1lem13  36312  dfsalgen2  46688  grtrimap  48297  pgn4cyclex  48475