Theorem simprr2 1241

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8144  icodiamlt  15585  psgnunilem2  19689  haust1  23650  cnhaus  23652  isreg2  23675  llynlly  23776  restnlly  23781  llyrest  23784  llyidm  23787  nllyidm  23788  cldllycmp  23794  txlly  23935  txnlly  23936  pthaus  23937  txhaus  23946  txkgen  23951  xkohaus  23952  xkococnlem  23958  cmetcaulem  25589  itg2add  26060  ulmdvlem3  26711  nosupprefixmo  28039  noinfprefixmo  28040  etaslts  28161  cutbdaybnd  28163  cutbdaybnd2  28164  addsproplem6  28342  negsproplem6  28401  mulsproplem13  28496  mulsproplem14  28497  mulsprop  28498  bdayfinbndlem1  28835  ax5seglem6  29494  n4cyclfrgr  30874  connpconn  35969  cvmlift3lem2  36054  cvmlift3lem8  36060  broutsideof3  36861  unblimceq0  37343  paddasslem10  40854  lhpexle2lem  41034  lhpexle3lem  41036  stoweidlem35  46989  stoweidlem56  47010  stoweidlem59  47013  pgn4cyclex  49168  2arwcat  50652