Theorem simprl2 1238

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8145  poxp3  8152  icodiamlt  15529  issubc3  17944  clsconn  23661  txlly  23868  txnlly  23869  itg2add  25993  ftc1a  26271  nosupprefixmo  27944  noinfprefixmo  27945  nosupbnd2  27960  noinfbnd2  27975  mulsprop  28403  bdayfinbndlem1  28740  f1otrg  29335  ax5seglem6  29399  axcontlem9  29437  axcontlem10  29438  clwwlkf  30525  locfinref  34359  erdszelem7  35784  btwnconn1lem13  36687  dfsalgen2  47177  grtrimap  48872  pgn4cyclex  49050