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  8148  poxp3  8155  icodiamlt  15515  issubc3  17931  clsconn  23624  txlly  23830  txnlly  23831  itg2add  25955  ftc1a  26233  nosupprefixmo  27901  noinfprefixmo  27902  nosupbnd2  27917  noinfbnd2  27932  mulsprop  28360  bdayfinbndlem1  28697  f1otrg  29257  ax5seglem6  29321  axcontlem9  29359  axcontlem10  29360  clwwlkf  30435  locfinref  34262  erdszelem7  35710  btwnconn1lem13  36612  dfsalgen2  47096  grtrimap  48754  pgn4cyclex  48932