Theorem simprl2 1227

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  poxp2  8087  poxp3  8094  icodiamlt  15395  issubc3  17811  clsconn  23417  txlly  23623  txnlly  23624  itg2add  25748  ftc1a  26026  nosupprefixmo  27686  noinfprefixmo  27687  nosupbnd2  27702  noinfbnd2  27717  mulsprop  28144  bdayfinbndlem1  28481  f1otrg  28961  ax5seglem6  29025  axcontlem9  29063  axcontlem10  29064  clwwlkf  30139  locfinref  34037  erdszelem7  35440  btwnconn1lem13  36342  dfsalgen2  46798  grtrimap  48453  pgn4cyclex  48631