Theorem simprl2 1216

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

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

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

This theorem is referenced by:  icodiamlt  14848  issubc3  17183  clsconn  22135  txlly  22341  txnlly  22342  itg2add  24464  ftc1a  24741  f1otrg  26769  ax5seglem6  26832  axcontlem9  26870  axcontlem10  26871  clwwlkf  27936  locfinref  31316  erdszelem7  32679  poxp2  33349  nosupprefixmo  33492  noinfprefixmo  33493  nosupbnd2  33508  noinfbnd2  33523  btwnconn1lem13  33976  dfsalgen2  43375