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  8093  poxp3  8100  icodiamlt  15400  issubc3  17816  clsconn  23395  txlly  23601  txnlly  23602  itg2add  25726  ftc1a  26004  nosupprefixmo  27664  noinfprefixmo  27665  nosupbnd2  27680  noinfbnd2  27695  mulsprop  28122  bdayfinbndlem1  28459  f1otrg  28939  ax5seglem6  29003  axcontlem9  29041  axcontlem10  29042  clwwlkf  30117  locfinref  33985  erdszelem7  35379  btwnconn1lem13  36281  dfsalgen2  46769  grtrimap  48424  pgn4cyclex  48602