Theorem simprr2 1224

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprr2	⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Proof of Theorem simprr2

Step	Hyp	Ref	Expression
1		simp2 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antll 730	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp2  8095  icodiamlt  15373  psgnunilem2  19436  haust1  23308  cnhaus  23310  isreg2  23333  llynlly  23433  restnlly  23438  llyrest  23441  llyidm  23444  nllyidm  23445  cldllycmp  23451  txlly  23592  txnlly  23593  pthaus  23594  txhaus  23603  txkgen  23608  xkohaus  23609  xkococnlem  23615  cmetcaulem  25256  itg2add  25728  ulmdvlem3  26379  nosupprefixmo  27680  noinfprefixmo  27681  etaslts  27801  cutbdaybnd  27803  cutbdaybnd2  27804  addsproplem6  27982  negsproplem6  28041  mulsproplem13  28136  mulsproplem14  28137  mulsprop  28138  bdayfinbndlem1  28475  ax5seglem6  29019  n4cyclfrgr  30378  connpconn  35448  cvmlift3lem2  35533  cvmlift3lem8  35539  broutsideof3  36339  unblimceq0  36726  paddasslem10  40194  lhpexle2lem  40374  lhpexle3lem  40376  stoweidlem35  46382  stoweidlem56  46403  stoweidlem59  46406  pgn4cyclex  48475  2arwcat  49948