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  14787  psgnunilem2  18615  haust1  21957  cnhaus  21959  isreg2  21982  llynlly  22082  restnlly  22087  llyrest  22090  llyidm  22093  nllyidm  22094  cldllycmp  22100  txlly  22241  txnlly  22242  pthaus  22243  txhaus  22252  txkgen  22257  xkohaus  22258  xkococnlem  22264  cmetcaulem  23892  itg2add  24363  ulmdvlem3  24997  ax5seglem6  26728  n4cyclfrgr  28076  connpconn  32595  cvmlift3lem2  32680  cvmlift3lem8  32686  noprefixmo  33315  scutbdaybnd  33388  broutsideof3  33700  unblimceq0  33959  paddasslem10  37125  lhpexle2lem  37305  lhpexle3lem  37307  stoweidlem35  42677  stoweidlem56  42698  stoweidlem59  42701