Theorem simprl2 1232

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  poxp2  8118  poxp3  8125  icodiamlt  15448  issubc3  17865  clsconn  23470  txlly  23676  txnlly  23677  itg2add  25801  ftc1a  26079  nosupprefixmo  27741  noinfprefixmo  27742  nosupbnd2  27757  noinfbnd2  27772  mulsprop  28200  bdayfinbndlem1  28537  f1otrg  29017  ax5seglem6  29081  axcontlem9  29119  axcontlem10  29120  clwwlkf  30195  locfinref  34099  erdszelem7  35511  btwnconn1lem13  36413  dfsalgen2  46879  grtrimap  48534  pgn4cyclex  48712