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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  poxp2  8140  poxp3  8147  icodiamlt  15491  issubc3  17907  clsconn  23568  txlly  23774  txnlly  23775  itg2add  25899  ftc1a  26177  nosupprefixmo  27842  noinfprefixmo  27843  nosupbnd2  27858  noinfbnd2  27873  mulsprop  28301  bdayfinbndlem1  28638  f1otrg  29198  ax5seglem6  29262  axcontlem9  29300  axcontlem10  29301  clwwlkf  30376  locfinref  34209  erdszelem7  35667  btwnconn1lem13  36569  dfsalgen2  47035  grtrimap  48690  pgn4cyclex  48868