Theorem simprl2 1219

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 726	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  poxp2  8131  poxp3  8138  icodiamlt  15386  issubc3  17803  clsconn  23154  txlly  23360  txnlly  23361  itg2add  25501  ftc1a  25778  nosupprefixmo  27427  noinfprefixmo  27428  nosupbnd2  27443  noinfbnd2  27458  mulsprop  27813  f1otrg  28377  ax5seglem6  28447  axcontlem9  28485  axcontlem10  28486  clwwlkf  29555  locfinref  33107  erdszelem7  34474  btwnconn1lem13  35363  dfsalgen2  45356