Theorem simprr2 1223

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8082  icodiamlt  15355  psgnunilem2  19417  haust1  23277  cnhaus  23279  isreg2  23302  llynlly  23402  restnlly  23407  llyrest  23410  llyidm  23413  nllyidm  23414  cldllycmp  23420  txlly  23561  txnlly  23562  pthaus  23563  txhaus  23572  txkgen  23577  xkohaus  23578  xkococnlem  23584  cmetcaulem  25225  itg2add  25697  ulmdvlem3  26348  nosupprefixmo  27649  noinfprefixmo  27650  etasslt  27764  scutbdaybnd  27766  scutbdaybnd2  27767  addsproplem6  27927  negsproplem6  27985  mulsproplem13  28077  mulsproplem14  28078  mulsprop  28079  ax5seglem6  28923  n4cyclfrgr  30282  connpconn  35290  cvmlift3lem2  35375  cvmlift3lem8  35381  broutsideof3  36181  unblimceq0  36562  paddasslem10  39938  lhpexle2lem  40118  lhpexle3lem  40120  stoweidlem35  46147  stoweidlem56  46168  stoweidlem59  46171  pgn4cyclex  48240  2arwcat  49715