Theorem simprr2 1219

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 1134	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antll 728	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  14856  psgnunilem2  18704  haust1  22066  cnhaus  22068  isreg2  22091  llynlly  22191  restnlly  22196  llyrest  22199  llyidm  22202  nllyidm  22203  cldllycmp  22209  txlly  22350  txnlly  22351  pthaus  22352  txhaus  22361  txkgen  22366  xkohaus  22367  xkococnlem  22373  cmetcaulem  24002  itg2add  24473  ulmdvlem3  25110  ax5seglem6  26841  n4cyclfrgr  28189  connpconn  32726  cvmlift3lem2  32811  cvmlift3lem8  32817  poxp2  33358  poxp3  33364  nosupprefixmo  33501  noinfprefixmo  33502  etasslt  33603  scutbdaybnd  33605  scutbdaybnd2  33606  broutsideof3  34012  unblimceq0  34271  paddasslem10  37440  lhpexle2lem  37620  lhpexle3lem  37622  stoweidlem35  43088  stoweidlem56  43109  stoweidlem59  43112