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 726	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 206  df-an 396  df-3an 1086

This theorem is referenced by:  poxp2  8123  icodiamlt  15379  psgnunilem2  19405  haust1  23178  cnhaus  23180  isreg2  23203  llynlly  23303  restnlly  23308  llyrest  23311  llyidm  23314  nllyidm  23315  cldllycmp  23321  txlly  23462  txnlly  23463  pthaus  23464  txhaus  23473  txkgen  23478  xkohaus  23479  xkococnlem  23485  cmetcaulem  25138  itg2add  25611  ulmdvlem3  26255  nosupprefixmo  27549  noinfprefixmo  27550  etasslt  27662  scutbdaybnd  27664  scutbdaybnd2  27665  addsproplem6  27807  negsproplem6  27861  mulsproplem13  27944  mulsproplem14  27945  mulsprop  27946  ax5seglem6  28661  n4cyclfrgr  30013  connpconn  34715  cvmlift3lem2  34800  cvmlift3lem8  34806  broutsideof3  35593  unblimceq0  35873  paddasslem10  39190  lhpexle2lem  39370  lhpexle3lem  39372  stoweidlem35  45236  stoweidlem56  45257  stoweidlem59  45260