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  8084  poxp3  8091  icodiamlt  15389  issubc3  17805  clsconn  23404  txlly  23610  txnlly  23611  itg2add  25735  ftc1a  26016  nosupprefixmo  27683  noinfprefixmo  27684  nosupbnd2  27699  noinfbnd2  27714  mulsprop  28141  bdayfinbndlem1  28478  f1otrg  28958  ax5seglem6  29022  axcontlem9  29060  axcontlem10  29061  clwwlkf  30137  locfinref  34006  erdszelem7  35400  btwnconn1lem13  36302  dfsalgen2  46784  grtrimap  48421  pgn4cyclex  48599