Theorem simprl2 1220

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8142  poxp3  8149  icodiamlt  15454  issubc3  17862  clsconn  23368  txlly  23574  txnlly  23575  itg2add  25712  ftc1a  25996  nosupprefixmo  27664  noinfprefixmo  27665  nosupbnd2  27680  noinfbnd2  27695  mulsprop  28085  f1otrg  28850  ax5seglem6  28913  axcontlem9  28951  axcontlem10  28952  clwwlkf  30028  locfinref  33872  erdszelem7  35219  btwnconn1lem13  36117  dfsalgen2  46370  grtrimap  47960