Theorem simprr2 1290

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 1168	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antll 721	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  icodiamlt  14515  psgnunilem2  18228  haust1  21485  cnhaus  21487  isreg2  21510  llynlly  21609  restnlly  21614  llyrest  21617  llyidm  21620  nllyidm  21621  cldllycmp  21627  txlly  21768  txnlly  21769  pthaus  21770  txhaus  21779  txkgen  21784  xkohaus  21785  xkococnlem  21791  cmetcaulem  23414  itg2add  23867  ulmdvlem3  24497  ax5seglem6  26171  n4cyclfrgr  27640  connpconn  31734  cvmlift3lem2  31819  cvmlift3lem8  31825  noprefixmo  32361  scutbdaybnd  32434  broutsideof3  32746  unblimceq0  33006  paddasslem10  35850  lhpexle2lem  36030  lhpexle3lem  36032  stoweidlem35  40995  stoweidlem56  41016  stoweidlem59  41019