Theorem simprl2 1215

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  icodiamlt  14795  issubc3  17119  clsconn  22038  txlly  22244  txnlly  22245  itg2add  24360  ftc1a  24634  f1otrg  26657  ax5seglem6  26720  axcontlem9  26758  axcontlem10  26759  clwwlkf  27826  locfinref  31105  erdszelem7  32444  noprefixmo  33202  nosupbnd2  33216  btwnconn1lem13  33560  dfsalgen2  42644