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  8162  icodiamlt  15610  psgnunilem2  19714  haust1  23675  cnhaus  23677  isreg2  23700  llynlly  23801  restnlly  23806  llyrest  23809  llyidm  23812  nllyidm  23813  cldllycmp  23819  txlly  23960  txnlly  23961  pthaus  23962  txhaus  23971  txkgen  23976  xkohaus  23977  xkococnlem  23983  cmetcaulem  25614  itg2add  26085  ulmdvlem3  26734  nosupprefixmo  28062  noinfprefixmo  28063  etaslts  28184  cutbdaybnd  28186  cutbdaybnd2  28187  addsproplem6  28365  negsproplem6  28424  mulsproplem13  28519  mulsproplem14  28520  mulsprop  28521  bdayfinbndlem1  28858  ax5seglem6  29517  n4cyclfrgr  30897  connpconn  36086  cvmlift3lem2  36171  cvmlift3lem8  36177  broutsideof3  36983  unblimceq0  37465  paddasslem10  40979  lhpexle2lem  41159  lhpexle3lem  41161  stoweidlem35  47138  stoweidlem56  47159  stoweidlem59  47162  pgn4cyclex  49317  2arwcat  50831