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  8187  icodiamlt  15634  psgnunilem2  19739  haust1  23700  cnhaus  23702  isreg2  23725  llynlly  23826  restnlly  23831  llyrest  23834  llyidm  23837  nllyidm  23838  cldllycmp  23844  txlly  23985  txnlly  23986  pthaus  23987  txhaus  23996  txkgen  24001  xkohaus  24002  xkococnlem  24008  cmetcaulem  25639  itg2add  26110  ulmdvlem3  26759  nosupprefixmo  28087  noinfprefixmo  28088  etaslts  28209  cutbdaybnd  28211  cutbdaybnd2  28212  addsproplem6  28390  negsproplem6  28449  mulsproplem13  28544  mulsproplem14  28545  mulsprop  28546  bdayfinbndlem1  28883  ax5seglem6  29542  n4cyclfrgr  30922  connpconn  36167  cvmlift3lem2  36252  cvmlift3lem8  36258  broutsideof3  37069  unblimceq0  37551  paddasslem10  41078  lhpexle2lem  41258  lhpexle3lem  41260  stoweidlem35  47250  stoweidlem56  47271  stoweidlem59  47274  pgn4cyclex  49429  2arwcat  50943