Theorem simprr2 1218

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  icodiamlt  14789  psgnunilem2  18617  haust1  21954  cnhaus  21956  isreg2  21979  llynlly  22079  restnlly  22084  llyrest  22087  llyidm  22090  nllyidm  22091  cldllycmp  22097  txlly  22238  txnlly  22239  pthaus  22240  txhaus  22249  txkgen  22254  xkohaus  22255  xkococnlem  22261  cmetcaulem  23885  itg2add  24354  ulmdvlem3  24984  ax5seglem6  26714  n4cyclfrgr  28064  connpconn  32477  cvmlift3lem2  32562  cvmlift3lem8  32568  noprefixmo  33197  scutbdaybnd  33270  broutsideof3  33582  unblimceq0  33841  paddasslem10  36959  lhpexle2lem  37139  lhpexle3lem  37141  stoweidlem35  42313  stoweidlem56  42334  stoweidlem59  42337