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  8082  poxp3  8089  icodiamlt  15355  issubc3  17766  clsconn  23355  txlly  23561  txnlly  23562  itg2add  25697  ftc1a  25981  nosupprefixmo  27649  noinfprefixmo  27650  nosupbnd2  27665  noinfbnd2  27680  mulsprop  28079  f1otrg  28859  ax5seglem6  28923  axcontlem9  28961  axcontlem10  28962  clwwlkf  30038  locfinref  33865  erdszelem7  35252  btwnconn1lem13  36154  dfsalgen2  46453  grtrimap  48062  pgn4cyclex  48240