Theorem simprr2 1224

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

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

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 1089

This theorem is referenced by:  poxp2  8087  icodiamlt  15365  psgnunilem2  19428  haust1  23300  cnhaus  23302  isreg2  23325  llynlly  23425  restnlly  23430  llyrest  23433  llyidm  23436  nllyidm  23437  cldllycmp  23443  txlly  23584  txnlly  23585  pthaus  23586  txhaus  23595  txkgen  23600  xkohaus  23601  xkococnlem  23607  cmetcaulem  25248  itg2add  25720  ulmdvlem3  26371  nosupprefixmo  27672  noinfprefixmo  27673  etasslt  27791  scutbdaybnd  27793  scutbdaybnd2  27794  addsproplem6  27956  negsproplem6  28015  mulsproplem13  28110  mulsproplem14  28111  mulsprop  28112  bdayfinbndlem1  28446  ax5seglem6  28990  n4cyclfrgr  30349  connpconn  35410  cvmlift3lem2  35495  cvmlift3lem8  35501  broutsideof3  36301  unblimceq0  36682  paddasslem10  40126  lhpexle2lem  40306  lhpexle3lem  40308  stoweidlem35  46315  stoweidlem56  46336  stoweidlem59  46339  pgn4cyclex  48408  2arwcat  49881