Theorem simprl2 1238

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8144  poxp3  8151  icodiamlt  15585  issubc3  18004  clsconn  23728  txlly  23935  txnlly  23936  itg2add  26060  ftc1a  26337  nosupprefixmo  28039  noinfprefixmo  28040  nosupbnd2  28055  noinfbnd2  28070  mulsprop  28498  bdayfinbndlem1  28835  f1otrg  29430  ax5seglem6  29494  axcontlem9  29532  axcontlem10  29533  clwwlkf  30620  locfinref  34455  erdszelem7  35931  btwnconn1lem13  36834  dfsalgen2  47295  grtrimap  48990  pgn4cyclex  49168