Theorem simprl2 1218

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  icodiamlt  15147  issubc3  17564  clsconn  22581  txlly  22787  txnlly  22788  itg2add  24924  ftc1a  25201  f1otrg  27232  ax5seglem6  27302  axcontlem9  27340  axcontlem10  27341  clwwlkf  28411  locfinref  31791  erdszelem7  33159  poxp2  33790  nosupprefixmo  33903  noinfprefixmo  33904  nosupbnd2  33919  noinfbnd2  33934  btwnconn1lem13  34401  dfsalgen2  43880