Theorem simprr2 1241

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 1155	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antll 742	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  8145  icodiamlt  15529  psgnunilem2  19628  haust1  23583  cnhaus  23585  isreg2  23608  llynlly  23709  restnlly  23714  llyrest  23717  llyidm  23720  nllyidm  23721  cldllycmp  23727  txlly  23868  txnlly  23869  pthaus  23870  txhaus  23879  txkgen  23884  xkohaus  23885  xkococnlem  23891  cmetcaulem  25522  itg2add  25993  ulmdvlem3  26645  nosupprefixmo  27944  noinfprefixmo  27945  etaslts  28066  cutbdaybnd  28068  cutbdaybnd2  28069  addsproplem6  28247  negsproplem6  28306  mulsproplem13  28401  mulsproplem14  28402  mulsprop  28403  bdayfinbndlem1  28740  ax5seglem6  29399  n4cyclfrgr  30779  connpconn  35822  cvmlift3lem2  35907  cvmlift3lem8  35913  broutsideof3  36714  unblimceq0  37212  paddasslem10  40710  lhpexle2lem  40890  lhpexle3lem  40892  stoweidlem35  46871  stoweidlem56  46892  stoweidlem59  46895  pgn4cyclex  49050  2arwcat  50534