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  8125  poxp3  8132  icodiamlt  15411  issubc3  17818  clsconn  23324  txlly  23530  txnlly  23531  itg2add  25667  ftc1a  25951  nosupprefixmo  27619  noinfprefixmo  27620  nosupbnd2  27635  noinfbnd2  27650  mulsprop  28040  f1otrg  28805  ax5seglem6  28868  axcontlem9  28906  axcontlem10  28907  clwwlkf  29983  locfinref  33838  erdszelem7  35191  btwnconn1lem13  36094  dfsalgen2  46346  grtrimap  47951  pgn4cyclex  48120