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  8068  icodiamlt  15337  psgnunilem2  19400  haust1  23260  cnhaus  23262  isreg2  23285  llynlly  23385  restnlly  23390  llyrest  23393  llyidm  23396  nllyidm  23397  cldllycmp  23403  txlly  23544  txnlly  23545  pthaus  23546  txhaus  23555  txkgen  23560  xkohaus  23561  xkococnlem  23567  cmetcaulem  25208  itg2add  25680  ulmdvlem3  26331  nosupprefixmo  27632  noinfprefixmo  27633  etasslt  27747  scutbdaybnd  27749  scutbdaybnd2  27750  addsproplem6  27910  negsproplem6  27968  mulsproplem13  28060  mulsproplem14  28061  mulsprop  28062  ax5seglem6  28905  n4cyclfrgr  30261  connpconn  35247  cvmlift3lem2  35332  cvmlift3lem8  35338  broutsideof3  36139  unblimceq0  36520  paddasslem10  39847  lhpexle2lem  40027  lhpexle3lem  40029  stoweidlem35  46052  stoweidlem56  46073  stoweidlem59  46076  pgn4cyclex  48136  2arwcat  49611